Programlama Teorilerini Birleştirme - Unifying Theories of Programming - Wikipedia

Programlama Teorilerini Birleştirme (UTP) içinde bilgisayar Bilimi ile fırsatlar program semantiği. Nasıl olduğunu gösterir gösterimsel anlambilim, operasyonel anlambilim ve cebirsel anlambilim için birleşik bir çerçevede birleştirilebilir resmi şartname tasarımı ve uygulaması programları ve bilgisayar sistemleri.

Bu başlığın kitabı C.A.R. Hoare ve O Jifeng yayınlandı Prentice Hall Uluslararası Bilgisayar Bilimleri Serisi 1998'de ve artık internette ücretsiz olarak mevcuttur.[1]

Teoriler

UTP'nin anlamsal temeli, birinci dereceden yüklem hesabı, ikinci dereceden mantıktan sabit nokta yapıları ile artırılmıştır. Geleneğini takiben Eric Hehner, programlar yüklemlerdir UTP'de ve anlamsal düzeyde programlar ve özellikler arasında bir ayrım yoktur. Sözleriyle Hoare:

Bir bilgisayar programı, o programı çalıştıran bir bilgisayarın davranışına ilişkin yapılabilecek her ilgili gözlemi tanımlayan en güçlü tahminle tanımlanır.[2]

UTP tabiriyle, bir teori belirli bir programlama paradigmasının bir modelidir. Bir UTP teorisi üç bileşenden oluşur:

  • bir alfabebir dış varlık tarafından gözlemlenebilen paradigmanın özniteliklerini belirten bir dizi değişken ismidir;
  • a imza, programlama dili kümesi olan paradigmaya içkin inşa eder; ve
  • koleksiyonu sağlık koşulları, paradigmaya uyan programların alanını tanımlayan. Bu sağlık koşulları tipik olarak şu şekilde ifade edilir: monoton etkisiz yüklem transformatörleri.

Program ayrıntılandırma UTP'de önemli bir kavramdır. Bir program tarafından rafine edildi ancak ve ancak yapılabilecek her gözlem aynı zamanda bir gözlemdir İyileştirmenin tanımı UTP teorilerinde ortaktır:

nerede gösterir[3] evrensel kapatma alfabedeki tüm değişkenler.

İlişkiler

En temel UTP teorisi, alfabe sınırlaması veya sağlıklılık koşulları olmayan alfabetik yüklemedir. İlişkiler teorisi biraz daha uzmanlaşmıştır, çünkü bir ilişkinin alfabesi yalnızca şunlardan oluşabilir:

  • dekore edilmemiş değişkenler (), uygulamanın başlangıcında programın bir gözlemini modellemek; ve
  • hazırlanmış değişkenler (), daha sonraki bir yürütme aşamasında programın bir gözlemini modelleme.

İlişkiler teorisinde bazı ortak dil yapıları şu şekilde tanımlanabilir:

  • Program durumunu hiçbir şekilde değiştirmeyen atlama ifadesi, ilişkisel kimlik olarak modellenmiştir:

  • Değer tahsisi değişkene ayar olarak modellenmiştir -e ve diğer tüm değişkenleri (ile gösterilir ) sabit:

  • Programlar arasında deterministik olmayan seçim, onların en büyük alt sınırıdır:

  • Koşullu seçim programlar arasında infix notasyonu kullanılarak yazılmıştır:

  • İçin bir anlambilim özyineleme tarafından verilir en az sabit nokta monotonik bir yüklem transformatörünün :

Referanslar

  1. ^ Hoare, C.A. R .; Jifeng, He (1 Nisan 1998). Programlama Teorilerini Birleştirme. Prentice Hall Koleji Bölümü. s. 320. ISBN  978-0-13-458761-5. Alındı 17 Eylül 2014.
  2. ^ C.A.R. Hoare, Programlama: Büyücülük mü bilim mi? IEEE Yazılımı, 1 (2): 5-16, Nisan 1984. ISSN  0740-7459. doi:10.1109 / MS.1984.234042.
  3. ^ Edsger W. Dijkstra ve Carel S. Scholten. Tahmin ve program semantiği. Bilgisayar Bilimlerinde Metinler ve Monograflar. Springer-Verlag New York, Inc., New York, NY, ABD, 1990. ISBN  0-387-96957-8.

daha fazla okuma

Dış bağlantılar