Yazan : Şadi Evren ŞEKER

Bilgisayar bilimlerinde, program doğrulama ( program corectness) için kullanılan mantığın ismidir. Basitçe bir dizi matematik kuralları ile bir programı modellemeye ve programın doğruluğunu ispatlamaya (veya yanlışlığını göstermeye) yarayan mantıktır.

Bu mantığın bilgisayar dünyasında bir dil olarak modellenmesi sonucunda yine bir muntazamn dil (formal language) ortaya çıkar. Yani aslında bir programın doğruluğu (correctness) başka bir program tarafından denetlenebilir.

İşte tam bu noktada Hoare mantığı devreye girer ve bir programın nasıl denetleneceğine cevap arar. Bu mantığa göre hoare üçlüsü ismi verilen bir yapıdan faydalanılır. Buna göre her komut satırı veya program satırı ayrı bir yapıdır ve aşağıdaki şekilde gösterilebilir:

{P} C {Q}

Bu gösterimde {} sembolleri arasında bulunan P ve Q programın çalışmasını doğrudan etkilemeyen ön ve son koşullardır (precondition postcondition). C ise ingilizcedeki command yani komut kelimesinin baş harfidir ve programlama dillerinde bulunan komutları ifade eder.

Yukarıdaki gösterimden anlaşılacağı üzere, bir programın doğruluğunu kontrol etmek için, programda bulunan her satırın ön koşulunu ve son koşulunu kontrol etme yaklaşımına hoare mantığı ismi verilir ve bu yaklaşımda şayet her komuttan önce doğru kontroller yapılır ve her satırdan sonra tam olarak beklenen durumlar belirlenirse programın doğruluğunun ispatlanabileceği iddia edilmektedir.

Bu yazı şadi evren şeker tarafından yazılmış ve bilgisayarkavramlari.com sitesinde yayınlanmıştır. Bu içeriğin kopyalanması veya farklı bir sitede yayınlanması hırsızlıktır ve telif hakları yasası gereği suçtur.

Hoare mantığının kendisine has bir gösterim şekli vardır. Buna göre programdaki komutlar ve bu komutlar arasındaki bağlantılar iki satır olarak gösterilir. Satırlardan üstteki, program komutlarını gösterirken alttaki de bu komutların hoare mantığındaki karşılığını gösterir.

Örnek hoare mantığı gösterimleri

Çok klasik olarak ihtiyaç duyulan bazı gösterimler aşağıda verilmiştir:

Boş komut

bossatir

Yukarıdaki gösterimde çizginin üzerinde herhangi bir komut bulunmamaktadır. Yani boş komut durumudur. Bu durumda komuttan önceki ve sonraki koşullar yani {P} aynıdır.

Ardışık iki komut

conj

Yukarıdaki iki ayrı satırın ( S ve T satırları) birleşimi (conjunction) gösterilmiştir. Bu işlemde S satırının son koşulu olan  ile T satırının ön koşulu olan Q aynı şarttır ve dolayısıyla iki satırın birleşmiş halinde ara koşul olacaktır. P ve R koşulları ise birleşmiş halin ön ve son koşulları olacaktır.

Koşullu komutlar

ifelse

Yukarıdaki gösterim veya operatörünün (disjunction) ifadesidir. Buna göre bir B koşuluna bağlı olarak S veya T satırlarından birisinin çalışması yukarıdaki gösterimle mümkündür. Buradaki gösterimde P ön koşulu ile B koşulu aynı anda olduğunda S satırı, P ön koşulu olup B koşulu olmadığında da T satırı çalışmıştır. Bunun anlamı P ön koşulu her zaman olmak kaydıyla şayet B doğruysa S yanlışsa T satırının çalışmasıdır.

Yorumlar

  1. Gözde

    Web sayfanızı doktora yeterlilik sınavına hazırlanırken keşfettim. Eksiklerimi tamamlamaya çalışırken, bazı konuların türkçe açıklamalarını sitenizden okumak ya da videolarını izlemek hızlı bir şekilde bütünü anlamama yardımcı oldu. Emeğiniz için teşekkürler çok sevap kazanıyorsunuz.

Gözde için bir cevap yazın Cevabı iptal et

E-posta hesabınız yayımlanmayacak. Gerekli alanlar * ile işaretlenmişlerdir