program sentezi

• verilen bir üst düzey belirtimi sağlayan bir programı otomatik olarak oluşturma işi.
  
  diğer otomatik programlama tekniklerinin aksine, belirtimler genellikle uygun bir mantıksal hesaplamanın algoritmik olmayan ifadeleridir. çoğu zaman, program sentezi, biçimsel doğrulama^* tekniklerini kullanır.
  
  1957'de cornell üniversitesi'nde alonzo church, matematiksel gereksinimlerden bir devreyi sentezleme problemini tanımladı. çalışma, sadece devrelere atıfta bulunsa ve programlardan bahsetmese bile, çalışma program sentezinin en erken tanımlarından biri olarak kabul edilir ve bazı araştırmacılar programın sentezine church'ün problemi adını verir. 1960'larda, otomatik programlayıcı oluşturmak için benzer bir fikir, yapay zeka araştırmacıları tarafından araştırıldı.
  
  o zamanlardan beri, çeşitli araştırma toplulukları program sentezi problemi üzerine düşündü. dikkat çeken çalışmalar arasında julius richard büchi ve lawrence landweber'in otomata-teorik yaklaşımı ve zohar manna ve richard waldinger'in çalışmaları yer alıyor. modern yüksek seviyeli programlama dillerinin gelişimi bile bir program sentezi biçimi olarak anlaşılabilir.
  
  son on yılda, biçimsel doğrulama topluluğunda ve ilgili alanlarda program sentezi düşüncesinde bir ilgi artışı görülmüştür. armando solar-lezama, programların otomatik olarak bulunması için program sentezi problemlerini boole mantığında kodlanmasının ve boole sağlanabilirlik problemi^* için algoritmaların kullanılmasının mümkün olduğunu gösterdi.
  
  2013 yılında, program sentezleme problemleri için birleşik bir çerçeve önerilmiştir ve 2014'ten beri www.sygus.org üzerinde farklı algoritmaların karşılaştırıldığı bir yıllık program sentezi yarışması vardır. yine de, mevcut algoritmalar sadece küçük programları sentezleyebilir.
  
  manna ve waldinger'in sistemi, kullanıcı tarafından verilen bir birinci dereceden belirtim formülünden başlar. bu formül için, bir kanıt oluşturulmaktadır, böylece fonksiyonel bir programı, birleştirici değiştirimlerden de sentezleyebilmektedir.
  
  bu sistem, ara formüllerin insan tarafından okunabilirliğini arttırmak için tasarlanmıştır: klasik çözümlemenin aksine, tümcecik normal biçim gerektirmez.
  
  program sentezi yöntemlerinden bazıları
  
  * biçimsel yöntem: sentezlenecek programın doğasını temsil eden mantıksal bir ifadeyle program sentezlenir ve otomatik olarak doğrulanır.
  * g/ç örneği: programlara girdi ve çıktıların bazı örnekleri gösterilerek bu girdileri ve çıktıları üreten programlar birleştirilir.
  * doğal dil anlayışı: doğal dilde yazılan program belirtimleri yorumlanır ve programlar sentezlenir.
  
  not: wikipedi erişimi engellemesinin abv. https://www.wikiwand.com/en/program_synthesis