Yazan : Şadi Evren ŞEKER
Bilgisayar bilimlerinde bir programın istenen özellikleri yerine getirip getirememesine verilen isimdir. Buna göre şayet bir program, beklenen özellikleri tam ve eksiksiz yerine getiriyor, istenmeyen sonuçlar ortaya çıkmıyor ve program başladıktan sonra her durumda başarılı bir şekilde bitiyorsa bu programa tam doğru ( total correctness) ismi verilir.
Durma probeleminden (halting problem) bilindiği üzere bir programın bitip bitmemesinin test edilmesi ayrı bir muammadır. Dolayısıyla tam doğru bir programın elde edilmesi veya ispatlanması farklı güçlükleri beraberinde getirir. Şayet bir program, kendinden beklenen özellikleri başarılı bir şekilde yerine getiriyor ancak bitip bitmemeyi garanti edemiyorsa (bir programın biteceği ispatlanamıyorsa) bu durumda programa kısmi doğru (partial correctness) ismi verilir.
Aslında programların doğruluğu (correctness), karar problemlerinin (decision problems) çözülmesidir.
Tam bu noktada bilgisayar bilimleri konusunda veciz sözleri ile konuya aydınlık getiren Dijkstranın bir sözünü hatırlamakta yarar var. “Testler hataların varlığını gösterebilir ama yokluğunu gösteremez.”
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.
Örneğin doğal sayılar kümesi üzerinde sayıların asal olup olmadığını test eden bir program yazdığımızı düşünelim. Bu program basitçe bir sayıyı alacak ve sayının çarpanlarını bulacaktır. Şayet sayının kendisi ve 1 dışında başka çarpanı yoksa bu sayıyı asal sayı ilan edecektir. Bu şekilde bir program yazmamızda herhangi bir sorun yoktur ancak programın biteceğini garanti edemeyiz. Elbette buradaki problem doğal sayıların bir sonu olup olmadığıdır. Yani program bütün asal doğal sayıları bulmaya çalışırsa sonsuz sayıda işlem yapması gerekir (ya da sonsuz bilinen bir değerse sonlu sayıda). Bu noktada bilgisayarın hafıza gibi kısıtları devreye girer. Yani sonsuz sayı işleyecek bir hafıza kapasitesi henüz bilgisayarlarda bulunmamaktadır.
Bu ispat sırasında programın bir lambda cebirine (lambda calculus) çevrilmesi ve bu cebirde doğruluğunun ispatlanması mümkündür. Bu tip ispat yöntemlerine program çıkarımı (program extraction) ismi verilir. Örneğin Curry Howard karşılığı (curry howard correspondence) yaklaşımı buna bir örnek olarak gösterilebilir.
Bir programın doğruluğunun tetkikine, program tetkiki (program verification) ismi verilir.
Program doğrulamanın kullanıldığı yerler
Program doğrulama, bir programın geliştirilme sürecinde, son adım olan test aşamasına gelinmeden hataların bulunması ve programın kodlanma hatta tasarım aşamasında hatalarının yakalanmasını sağladığı için oldukça önemlidir. Örneğin bitmiş bir programdaki bir hatanın test ile bulunması bütün tasarım ve kodlama adımlarına geri dönülmesini ve dolayısıyla hatanın telafisi için harcanan maliyetin yüksek olmasını sağlarken, daha henüz kodlama aşamsında hatanın tespiti maliyeti düşürmektedir.
Ayrıca yazılan programın hatasının test aşamasında hiçbir zaman bulunamaması da söz konusu olabilir. Bu ihtimale karşı programın matematiksel olarak doğruluğunun ispatlanması çok önemlidir.