Tony Hoare'ın Doğruluk Fikirleri: Mantıktan Güvenli Koda

Neden “doğruluk” "çalışıyor gibi görünmek"ten daha fazlasıdır

İnsanlar bir programın "doğru" olduğunu söylediklerinde genellikle kastedilen şudur: "Birkaç kez çalıştırdım ve çıktı doğru görünüyordu." Bu faydalı bir işarettir—ama doğruluk bu değildir. Basitçe söylemek gerekirse, doğruluk programın spesifikasyonunu karşılaması demektir: izin verilen her giriş için gerekli sonucu üretir ve durum değişiklikleri, zamanlama ve hatalarla ilgili kurallara uyar.

Yakınlaşma şu ki: "spec'i karşılamak" kulağa olduğundan daha zordur.

Doğruluk gerçekten neden zor

İlk olarak, spesifikasyonlar çoğunlukla belirsizdir. Bir ürün gereksinimi "listeyi sırala" diyebilir, ama bu stabil sıralama mı demektir? Aynı değerlere ne olacak, boş listeler veya sayısal olmayan öğeler? Eğer spec söylemiyorsa, farklı kişiler farklı varsayımlarda bulunacaktır.

İkinci olarak, uç durumlar nadir değildir—sadece daha az test edilirler. Null değerler, taşma, off-by-one sınırları, sıra dışı kullanıcı etkileşimleri ve beklenmedik dış hatalar "çalışıyormuş gibi" görünen şeyi üretimde başarısızlığa çevirebilir.

Üçüncü olarak, gereksinimler değişir. Bir program dünün spesifikasyonuna göre doğruyken bugünün spesifikasyonuna göre yanlış olabilir.

Bu yazının geri kalanından ne beklemelisiniz

Tony Hoare'ın büyük katkısı her şeyi her zaman ispatlamamız gerektiğini söylemek değildi. Asıl fikir, kodun ne yapması gerektiği konusunda daha kesin olabileceğimiz ve bunu disiplinli bir şekilde akıl yürütebileceğimizdi.

Bu yazıda üç bağlantılı ipliği takip edeceğiz:

• Hoare mantığı: ön koşullar ve son koşullar kullanarak hafif, yapılı akıl yürütme.
• Quicksort: partition gibi küçük "bariz" adımların dikkatli düşünmeyi nasıl gerektirdiğini gösteren tanıdık bir algoritma.
• Güvenlik zihniyeti: başarısızlıkların gerçek sonuçları olduğunda doğruluk bir pratik sorumluluktur.

Çoğu ekip tam formal kanıtlar yazmayacaktır. Ama kısmi, "kanıt tarzı" düşünme bile hataları bulmayı kolaylaştırır, incelemeleri keskinleştirir ve kod gönderilmeden önce davranışı netleştirir.

Tony Hoare kısa: günlük koda ulaşan fikirler

Tony Hoare, çalışmalarının makalelerde veya sınıf dışına çıkmayan nadir bilgisayar bilimcilerinden biridir. Akademi ile sanayi arasında hareket etti ve her ekibin hâlâ karşılaştığı pratik bir soruna önem verdi: özellikle risk yüksek olduğunda bir programın düşündüğümüz şeyi yaptığını nasıl bilebiliriz?

Bu yazı için önemli katkılar

Bu makale, gerçek kod tabanlarında sıkça görülen birkaç Hoare fikrine odaklanır:

• Hoare mantığı: program davranışını ön koşullar, son koşullar ve iyi bilinen Hoare üçlüsü {P} C {Q} ile tanımlama yolu.
• Döngü invariantları: döngüler hakkında "makinemde çalıştı"nın ötesinde akıl yürütme alışkanlığı.
• Quicksort (özellikle partition adımı): doğruluğun küçük, kesin ifadelerinin çok şeyi açıkladığı ünlü bir örnek.
• Güvenlik düşüncesi: doğruluk lüks bir özellik değil; rahatsızlıktan zarara kadar fark yaratabilecek bir sorumluluktur.

Bu yazıda ne yapmayacağız

Burada derin matematiksel formalizm bulmayacaksınız ve Quicksort'un makine tarafından doğrulanmış tam bir ispatını yapmayacağız. Amaç kavramları erişilebilir tutmak: akıl yürütmenizi netleştirecek kadar yapı, kod incelemelerinizi bir lisansüstü seminere çevirmeyecek kadar sade.

Çalışmalarının günlük programlamayı neden etkilediği

Hoare'ın fikirleri sıradan kararlara dönüşür: bir fonksiyonun hangi varsayımlara dayandığı, çağıranlara neyi garanti ettiği, bir döngüde yarıda neyin doğru kalması gerektiği ve incelemelerde "neredeyse doğru" değişiklikleri nasıl fark edeceğiniz. {P} C {Q}'yi açıkça hiç yazmasanız bile bu biçimde düşünmek API'leri, testleri ve karmaşık kod hakkındaki tartışmaların kalitesini artırır.

Doğruluk pratikte ne demektir

Hoare'ın görüşü "birkaç örneği geçti" demekten daha katıdır: doğruluk üzerinde anlaşılmış bir vaadi karşılamaktır, küçük bir örneklemde doğru görünmek değil.

Gereksinimler vs. spesifikasyon vs. uygulama

• Gereksinimler işin sade dildeki ihtiyacıdır (paydaşların istediği).
• Spesifikasyon o ihtiyacın kesin, kontrol edilebilir versiyonudur (fonksiyonun ne yapması gerektiği).
• Uygulama yazdığınız koddur (nasıl yaptığı).

Hatalar genellikle ekipler ortadaki adımı atladığında olur: gereksinimden doğrudan koda atlanır ve "söz" bulanık kalır.

Kısmi doğruluk vs. toplam doğruluk

Sıkça karışan iki iddia vardır:

• Kısmi doğruluk: kod dönerse, sonuç doğrudur.
• Toplam doğruluk: kod döner ve sonuç doğrudur. (yani sonlanma iddiaya dahildir)

Gerçek sistemlerde, "hiç bitmemek" yanlış cevap vermek kadar zararlı olabilir.

Doğruluk her zaman varsayımlara bağlıdır

Doğruluk ifadeleri evrensel değildir; şu tür varsayımlara dayanır:

• Girdiler (örn. liste belleğe sığar, öğeler karşılaştırılabilir)
• Kısıtlar (örn. zaman sınırları, tamsayı aralıkları)
• Ortam (örn. eşzamanlılık, I/O hataları, konfigürasyon)

Varsayımları açık etmek "makinemde çalışıyor" u başkalarının da akıl yürütebileceği bir şeye çevirir.

Küçük bir örnek spesifikasyon

sortedCopy(xs) fonksiyonunu düşünün.

Faydalı bir spec şöyle olabilir: "Yeni bir liste ys döndürür öyle ki (1) ys artan sırada sıralıdır, ve (2) ys xs ile tam olarak aynı elemanları içerir (aynı sayılarla), ve (3) xs değişmemiştir."

Şimdi "doğru" demek, kodun bu üç noktayı belirtilen varsayımlar altında sağlamasıdır—çıktının hızlı bir testte sıralı görünmesi değil.

Hoare mantığı temelleri: ön koşullar, son koşullar, üçlüler

Hoare mantığı, kodu bir sözleşme gibi konuşma yoludur: eğer belirli varsayımları sağlayan bir durumda başlarsanız ve bu kodu çalıştırırsanız, belirli garantileri sağlayan bir durumda bitireceksiniz.

Temel notasyon Hoare üçlüsüdür:

{precondition} program {postcondition}

Ön koşullar: neyi varsayıyorsunuz

Bir ön koşul, program parçası çalışmadan önce doğru olması gerekenleri belirtir. Bu, umduğunuz değil; kodun ihtiyacı olan şeydir.

Örnek: iki sayının ortalamasını taşma kontrolü olmadan döndüren bir fonksiyon olsun.

• Precondition: a + b tamsayı tipine sığar
• Program: avg = (a + b) / 2
• Postcondition: avg matematiksel ortalamaya eşittir

Eğer ön koşul sağlanmıyorsa (taşma mümkünse), postcondition vaadi artık geçerli değildir. Üçlü bunu yüksek sesle söylemenizi sağlar.

Son koşullar: neyi garanti ediyorsunuz

Bir son koşul, kod çalıştıktan sonra neyin doğru olacağını belirtir—ön koşul sağlandığı varsayılarak. İyi son koşulları somut ve test edilebilir yazın. "Sonuç geçerli" demek yerine "geçerli"nin ne anlama geldiğini söyleyin: sıralı, negatif olmayan, aralık içinde, sadece belirli alanlarda değişmiş vb.

Atama ve sıralama (simgesel karmaşaya girmeden)

Hoare mantığı küçük ifadelerden çok adımlı koda kadar ölçeklenir:

• Atama durumu kesin olarak değiştirir. Düşünme sorusu: x = x + 1 sonrası x hakkında hangi gerçekler doğrudur?
• Sıralama (önce bunu sonra şunu yap) garantileri zincirler: adım 1, adım 2 için ön koşulu sağlıyorsa tüm blok daha güvenilir olur.

Amaç her yerde süslü sözdizimi kullanmak değildir. Amaç niyeti okunur hâle getirmektir: açık varsayımlar, açık sonuçlar ve incelemelerde daha az "görünüşte çalışıyor" tartışması.

Gerçek ekiplerin yazabileceği döngü invariantları

Bir döngü invariantı, döngü başlamadan önce doğru olan, her yinelemeden sonra doğru kalan ve döngü bittiğinde hâlâ geçerli olan bir ifadedir. Basit ama büyük fayda sağlar: "çalışıyor gibi" mantığını, her adımda aslında kontrol edilebilecek bir iddiaya dönüştürür.

Neden invariantlar gevezeliğe son verir

Invariant yoksa, bir inceleme sık sık şöyle olur: "Liste üzerinde yineleyip yavaş yavaş işleri düzeltiyoruz." Bir invariant netlik zorunluluğu getirir: şu anda tam olarak ne doğru? Döngü bitmemişken bile. Bunu net söyleyebildiğinizde, off-by-one hataları ve eksik durumlar invariantın bozulduğu anlarda görünür hale gelir.

Yeniden kullanılabilir invariant şablonları

Günlük kodun çoğu birkaç güvenilir şablonu kullanabilir.

1. Sınırlar / indeks güvenliği

İndeksleri güvenli aralıkta tutun.

• 0 <= i <= n
• low <= left <= right <= high

Bu invariant türü aralık dışı erişimi önlemekte ve dizi akıl yürütmesini somutlaştırmakta iyidir.

2. İşlenmiş vs. işlenmemiş öğeler

Verilerinizi "tamamlanmış" ve "henüz" bölgelerine ayırın.

• "a[0..i)'daki tüm elemanlar incelendi."
• "result'a taşınan her öğe filtre koşulunu sağlar."

Bu, belirsiz ilerlemeyi neyin "işlendiği" olarak tanımlar.

3. Sıralı önek (veya partition edilmiş önek)

Sıralama, birleştirme ve partitioning'te yaygın.

• "a[0..i) sıralıdır."
• "a[0..i)'deki tüm öğeler <= pivot, ve a[j..n)'deki tüm öğeler >= pivot."

Dizinin tamamı henüz sıralı olmasa bile neyin sabitlendiğini belirtirsiniz.

Düz Türkçe: sonlanma için küçülen bir ölçü

Doğruluk sadece doğru olmakla ilgili değildir; döngünün ayrıca bitmesi gerekir. Bunun tartışması için genellikle her yinelemede azalan bir ölçü (variant) isimlendirilir ve bunun sonsuza dek azalması mümkün değildir.

Örnekler:

• "n - i her seferinde 1 azalır."
• "İşlenmemiş öğe sayısı azalır."

Küçülen bir ölçü bulamıyorsanız, sonsuz döngü riski olabilir.

Quicksort: koda dair akıl yürütme örnek çalışması

Quicksort'un basit bir vaadi vardır: bir dilimi (veya dizi segmentini) verilen elemanları kaybetmeden veya yeni değerler icat etmeden artan sıraya dizmek. Algoritmanın yüksek seviyedeki şekli kolayca özetlenir:

1. Bir pivot değeri seçin.
2. Aralığı partition edin öyle ki "pivottan küçük" öğeler bir tarafa, "pivottan büyük" öğeler diğer tarafa gelsin ("eşit" için bir kural ile).
3. Sol ve sağ alt aralıklarda özyineleme yapın.

Bu, doğruluk için öğretici bir örnektir çünkü kafada tutulabilecek kadar küçük ama gayri resmi akıl yürütmenin nerede başarısız olabileceğini gösterecek kadar zengindir. Rastgele birkaç testte "çalışıyor gibi" duran bir Quicksort, belirli girdiler veya sınır durumlarında yine de yanlış olabilir.

"Bariz" uygulamaları bozan tuzaklar

Birkaç konu çoğu hataya neden olur:

• Çoğaltmalar: Partition "eşit" elemanları tutarsız ele alırsa, alt aralıklar küçülmeyebilir (sonsuz özyineleme) veya partition kendi kuralını ihlal edebilir.
• Boş veya tek öğeli aralıklar: Temel durum kesin olmalı; aksi halde indeks dışı erişim veya sonsuz özyineleme olur.
• Off-by-one indeksleri: Partition algoritmaları genellikle iki işaretçi kullanır; tek bir yanlış karşılaştırma veya artırma öğeleri atlayabilir veya aralığın dışında takas yapabilir.

Gerçekte neyi ispatlamalısınız

Hoare tarzı akıl yürütmede ispatınızı tipik olarak iki parçaya ayırırsınız:

• Partition doğruluğu: partition işleminden sonra sol taraftaki her öğe pivot ile seçilen ilişkiye uyar, sağ taraftaki her öğe zıt ilişkiye uyar ve sonuç orijinal elemanların bir permutasyonudur.
• Özyineleme doğruluğu: özyinelemeler kesinlikle daha küçük aralıklarda çalışır (sonlanma) ve, alt aralıkları sıralayacaklarını varsayarsak, tüm aralığın sıralı olduğu sonucuna varılır.

Bu ayrım akıl yürütmeyi yönetilebilir kılar: partition'ı doğru yapın, sonra sıralama doğruluğunu bunun üzerine inşa edin.

Partition doğruluğu: Quicksort'un özü

Quicksort'un hızı görünüşte küçük bir yordamdan—partition—bağımlıdır. Partition biraz hatalı olsa bile Quicksort yanlış sıralama, sonsuz döngü veya uç durumlarda çökme yapabilir.

Partition sözleşmesi (ne garanti etmelidir)

Klasik Hoare partition şemasını (içeri doğru hareket eden iki işaretçi) kullanacağız.

Girdi: bir dizi dilimi A[lo..hi] ve seçilmiş bir pivot değeri (genellikle A[lo]).

Çıktı: bir p indeksi öyle ki:

• A[lo..p] içindeki her öğe <= pivot
• A[p+1..hi] içindeki her öğe >= pivot

Sözleşmede vaadedilmeyen şeye dikkat edin: pivot mutlaka p pozisyonunda bitmeyebilir ve pivot'a eşit öğeler her iki tarafta da bulunabilir. Bu sorun değil—Quicksort sadece doğru bir bölünmeye ihtiyaç duyar.

Tarama ve takas sırasında ana invariantlar

Algoritma iki indeksi ilerletirken—soldan i, sağdan j—iyi akıl yürütme zaten "kilitlenmiş" olanı odaklanır. Pratik bir invariant seti şudur:

• A[lo..i-1] içindeki tüm öğeler <= pivot (sol taraf temiz)
• A[j+1..hi] içindeki tüm öğeler >= pivot (sağ taraf temiz)
• A[i..j] içindeki her şey sınıflandırılmamış (hala kontrol edilecek)

Eğer A[i] >= pivot ve A[j] <= pivot bulunursa, bunları takas etmek bu invariantları korur ve sınıflandırılmamış orta bölgeyi daraltır.

Doğruluğun kapsaması gereken uç durumlar

• Hepsi pivot'tan küçük: i sağa kadar koşar; partition yine de sonlanmalı ve mantıklı bir p döndürmelidir.
• Hepsi pivot'tan büyük: j sola kadar koşar; aynı sonlanma kaygısı vardır.
• Birçok eşit: karşılaştırmalar tutarsızsa (< vs <=) işaretçiler takılabilir. Hoare şeması ilerlemenin sürmesi için tutarlı bir kural gerektirir.
• Zaten sıralı / ters sıralı: performans bozulabilir ama sözleşme kırılmamalıdır.

Lomuto, Hoare, üç-yollu partition gibi farklı şemalar vardır. Önemli olan birini seçmek, onun sözleşmesini belirtmek ve kodu o sözleşmeye karşı tutarlı şekilde incelemektir.

Özyineleme hakkında akıl yürütme: temel durumlar ve sonlanma

Özyineleme hakkında güven duymak, iki soruya net cevap verebildiğinizde en kolaydır: ne zaman durur? ve her adım neden geçerli? Hoare tarzı düşünce buna yardımcı olur çünkü çağrıdan önce neyin doğru olması gerektiğini ve döndüğünde ne olacağını açıkça ifade etmenizi zorlar.

Temel durum doğru olmalıdır

Bir özyinelemeli fonksiyonun, daha fazla özyineleme yapmadığı en az bir temel durumu olmalı ve yine de vaat edilen sonucu sağlamalıdır.

Sıralama için tipik temel durum "uzunluğu 0 veya 1 olan diziler zaten sıralıdır". Burada "sıralı"yı açıkça söyleyin: ≤ sıralama ilişkisi için, her i < j için a[i] ≤ a[j] olmalıdır. (Eşit öğelerin orijinal sırayı koruyup korumadığı ayrı bir özellik olan stabilite ile ilgilidir; Quicksort genelde stabil değildir, tasarlamazsanız.)

Alt problem küçülmelidir

Her özyineleme adımı kendisini kesinlikle daha küçük bir girdi üzerinde çağırmalıdır. Bu "küçülme" sonlanma argümanıdır: boyut azalıyor ve 0'ın altına inemez, dolayısıyla sonsuza dek özyineleyemezsiniz.

Küçülme aynı zamanda yığın güvenliği için önemlidir. Doğru kod bile özyineleme derinliği çok büyükse çökebilir. Quicksort'ta dengesiz partition'lar derin özyinelemeye neden olabilir. Bu hem sonlanma ispatı hem de pratik bir uyarıdır.

Önce doğruluk, sonra performans

Quicksort'un kötü durum zaman karmaşıklığı, çok dengesiz partition'larda O(n²)'ye düşebilir, ama bu performans meselesidir—doğruluk hatası değildir. Buradaki akıl yürütme hedefi şudur: partition elemanları koruyup pivot'a göre doğru şekilde böldüğü sürece, alt aralıkların özyinelemeli sıralanması tüm aralığın tanım gereği sıralı olmasını sağlar.

İspat-tarzı düşünme ve test: birbirlerine nasıl uyar

Testler ve ispat-tarzı akıl yürütme aynı hedefe—güvene—ulaşmak ister ama farklı yollar izler.

Testler hataları bulur; akıl yürütme hata sınıflarını ortadan kaldırır

Testler somut hataları yakalamada mükemmeldir: bir off-by-one, eksik bir uç durum, bir regresyon. Ama bir test süiti yalnızca giriş uzayını örnekler. "%100 kapsama" bile "tüm davranışların kontrolü" anlamına gelmez; çoğunlukla "tüm satırlar çalıştırıldı" demektir.

İspat-tarzı akıl yürütme (özellikle Hoare stili), bir spesifikasyondan başlar ve sorar: bu ön koşullar sağlandığında kod her zaman son koşulları kuruyor mu? Bunu iyi yaptığınızda sadece bir hatayı bulmazsınız—çoğu zaman bir hata kategorisini ortadan kaldırırsınız (ör. dizi erişimleri sınırlar içinde kalır veya döngü partition özelliğini bozmadan devam eder).

Spesifikasyonlar daha iyi testler üretir

Açık bir spec bir test üreticisidir.

Eğer postcondition "çıktı sıralıdır ve girdinin permutasyonudur" diyorsa, otomatik olarak test fikirleri elde edersiniz:

• Sınırlar: boş liste, tek öğe, zaten sıralı, ters sıralı.
• Invariantlar: ara özellikler (örn. partition sol tarafı <= pivot tutar).
• Geçersiz girdiler: null'lar, NaN, aralık dışı indeksler, tutarsız karşılaştırıcılar.

Spec size "doğru"nun ne olduğunu söyler; testler gerçeğin ona uyup uymadığını kontrol eder.

Özellik tabanlı testler: ispat ile örnek arası köprü

Özellik tabanlı testler, kanıtla örnek arasındaki köprüdür. Birkaç örnek seçmek yerine özellikleri belirtirsiniz ve araç birçok girdi üretir.

Sıralama için iki basit özellik çok iş görür:

• Sıralı olma: sonuç non-decreasing sıradadır.
• Permutasyon: sonuç girdinin tam olarak aynı elemanlarını içerir.

Bu özellikler esasen postcondition'ların yürütülebilir kontrolleridir.

Ekiplerin gerçekten kullanabileceği iş akışı

Ölçeklenebilir hafif rutin:

1. Önce bir spec yazın (ön koşullar, son koşullar, ana invariantlar).
2. Zor kısımları düşünün (döngüler, partition, özyineleme sınırları).
3. Spesifikasyonu testlere dönüştürün (sınır durumlar + özellik tabanlı testler).
4. Bunları kodda ve incelemelerde birlikte tutun, böylece gelecekteki değişiklikler sessizce orijinal niyeti bozamaz.

Bunu kurumsallaştırmak isterseniz, "spec + akıl notları + testler"i PR şablonunuzun veya kod inceleme kontrol listenizin bir parçası yapın (bakınız /blog/code-review-checklist).

Eğer sohbet tabanlı arayüzden kod üreten bir vibe-coding iş akışı kullanıyorsanız, aynı disiplin geçerlidir—hatta daha da önemli. Koder.ai gibi araçlarda Planlama Modu'nda ön koşulları/son koşulları sabitleyip sonra kod üretmek, snapshot ve rollback ile yineleme yaparken özellik testleri eklemek işleri hızlandırır; ama spec hâlâ "hızlı"nin "kırılgan"a dönüşmesini engeller.

Güvenlik düşüncesi: gerçek dünya sonuçları olan doğruluk

Doğruluk yalnızca "program doğru değeri döndürür" ile ilgili değildir. Güvenlik düşüncesi farklı bir soru sorar: hangi sonuçlar kabul edilemez ve kod baskılandığında, kötü kullanıldığında veya kısmen başarısız olduğunda onları nasıl önleriz? Pratikte güvenlik, bir önceliklendirme sistemi ile doğruluktur: bazı hatalar sadece can sıkıcıdır, bazıları finansal kayıp, gizlilik ihlali veya fiziksel zarar yaratabilir.

Tehlikeler vs. hatalar: etkisi neden önemlidir

Bir bug kodda veya tasarımda bir kusurdur. Bir tehlike (hazard) kabul edilemez bir sonuca yol açabilecek durumdur. Bir hata bir bağlamda zararsız, başka bağlamda tehlikeli olabilir.

Örnek: bir fotoğraf galerisi içindeki bir off-by-one hata bir resmi yanlış etiketleyebilir; aynı hata bir ilaç doz hesaplayıcısında hastaya zarar verebilir. Güvenlik düşüncesi kod davranışını sonuçlarla ilişkilendirmenizi zorunlu kılar, sadece "spec uyumu" ile değil.

En kötü sonuçları önleyen basit teknikler

Ağır formal yöntemlere gerek yok; ekipler küçük, tekrarlanabilir uygulamalar benimseyerek hemen fayda sağlar:

• Güvenli başarısızlık varsayılanı: Sistem emin olmadığında daha güvenli davranışı seçin. Örneğin yetkilendirme kontrolleri hata verdiğinde "izin ver" yerine "reddet".
• Sınırda giriş doğrulama: kullanıcı girdilerini, dosya içeriklerini ve ağ verilerini güvensiz kabul edin. Tipleri, aralıkları, formatları ve invariantları erkenden doğrulayın.
• Limitler ve zaman aşımı: bellek kullanımı, istek boyutları, özyineleme derinliği, tekrar sayıları ve yürütme süresi için üst sınırlar koyun. Birçok olay "doğru" kodun mantıksız girdilerle çalışması sonucu oluşur.

Bu teknikler Hoare tarzı akıl yürütme ile doğal olarak eşlik eder: ön koşulları açıkça yaparsınız (hangi girdiler kabul edilebilir) ve son koşullar güvenlik özelliklerini içerir (hangi durumlar asla olmamalı).

Takaslar: kontroller bedava değil

Güvenlik kontrollerinin bir maliyeti vardır—CPU zamanı, karmaşıklık veya bazen yanlış reddetme.

• Performans vs. kontroller: hızlı yollar değerli ama kritik sınırlar doğrulama, oran sınırlama ve zaman aşımı gerektirir.
• Sertlik vs. kullanılabilirlik: tüm kusurlu girişleri reddetmek kullanıcıları rahatsız edebilir; her şeyi kabul etmek belirsizlik ve sömürüye yol açabilir. Pratik bir uzlaşma: "çekirdekte sert, kenarlarda esnek" olurken kenar durumları loglayıp ne sıklıkta olduklarını ölçün.

Güvenlik düşüncesi zerafeti kanıtlamaktan ziyade karşılanamayacak hata modlarını önlemeye odaklanır.

Hoare tarzı akıl yürütmeyi kod incelemelerine uygulamak

Kod incelemeleri doğruluk düşüncesinin en hızlı karşılığını verdiği yerdir; çünkü eksik varsayımları üretime gitmeden önce fark edebilirsiniz. Hoare'ın temel hareketi—önceden hangi koşullar doğru olmalı ve sonra ne olacak—inceleme sorularına kolayca dönüşür.

Hoare fikirlerini inceleme sorularına çevirin

Bir değişikliği okurken her önemli fonksiyonu küçük bir sözleşme gibi çerçevelemeye çalışın:

• Varsayımlar (preconditions): girdiler, durum ve çevre hakkında ne doğru olmalı? (örn. "liste boş değil", "kullanıcı kimlik doğrulandı", "kilit alınmış").
• Garantiler (postconditions): döndükten sonra ne doğru olacak, dönen değerler ve yan etkiler dahil? (örn. "bakiye miktarı kadar azaldı", "kayıt yalnızca bir kez eklendi").
• Invariantlar: bir döngü, tekrar veya çok adımlı iş akışı boyunca ne kalmalı? (örn. "işlenmiş_sayı ≤ toplam", "şu ana kadar debit toplamı ile kredi toplamı eşit").
• Hata davranışı: hatada sistem güvenli durumda bırakılıyor mu? Kısmi güncellemeler geri alınıyor mu?

Basit bir gözlemci alışkanlığı: pre/post koşullar bir cümlede söylenemiyorsa, kod muhtemelen daha net bir yapıya ihtiyaç duyar.

Kritik fonksiyonlar için “kontrat yorumları”

Riskli veya merkezi fonksiyonların imzasının hemen üstüne küçük bir kontrat yorumu ekleyin. Somut tutun: girdiler, çıktılar, yan etkiler ve hatalar.

def withdraw(account, amount):
    """Contract:
    Pre: amount is an integer > 0; account is active.
    Post (success): returns new_balance; account.balance decreased by amount.
    Post (failure): raises InsufficientFunds; account.balance unchanged.
    """
    ...

Bu yorumlar formal bir ispat değildir ama inceleyicilere kontrol edecekleri somut bir şey verir.

Riskli kod için hafif kontrol listesi

Aşağıdaki konularla ilgilenen kodu incelerken ekstra açık olun:

• Parslama/doğrulama (bozuk girdi yolları, sınır durumları)
• Eşzamanlılık (kilitler, yarışlar, idempotentlik, tekrarlar)
• Para/kota (yuvarlama, çift ödeme, taşma)
• İzinler (kim ne yapabilir ve neden)

Eğer değişiklik bunlardan herhangiğine dokunuyorsa, sorun: "Önkoşullar nerede zorlanıyor?" ve "Bir şey başarısız olursa hangi garantileri sağlamaya devam ediyoruz?"

Ne zaman formal araçlar kullanılmalı—pratik bir kontrol listesi

Formal akıl yürütme bütün kod tabanınızı matematiksel bir makale haline getirmek zorunda değildir. Ama ekstra kesinliğe yatırım yapmak mantıklıdır: "testlerde iyi görünüyor"nun yeterli olmadığı yerlere.

Formal yöntemlerin en çok yardımcı olduğu yerler

Küçük, kritik bir modül her şeyin dayandığı yer olduğunda (auth, ödeme kuralları, izinler, güvenlik kilitleri) veya off-by-one hatalarının aylarca saklanabildiği karmaşık bir algoritmada (parser'lar, zamanlayıcılar, önbellek/çıkarmalar, partition tarzı kod, sınır ağır veri dönüşümleri) formal yöntemler uygundur.

Kullanışlı bir kural: bir hata gerçek zarar, büyük finansal kayıp veya sessiz veri bozulmasına yol açabiliyorsa, sıradan inceleme+testten fazlasını isteyin.

Düşünülmesi gereken araçlar (yüksek seviyede)

Hafiften ağır ağırlığa çeşitli seçenekler vardır ve sıkça en iyi sonuçlar bunların kombinasyonundan çıkar:

• Tipler (güçlendirilmiş tip sistemleri, non-null, birimler/miktarlar): geçersiz durumların önünü keser.
• Statik analiz: şüpheli yollar, API hatalı kullanımları, veri yarışları, kirli giriş akışlarını bulur.
• Kontratlar (ön/son koşullar, assertler): Hoare tarzı ifadelerin yürütülebilir versiyonları.
• Model kontrol: durum makinelerini keşfeder (protokoller, eşzamanlılık ve "ya ne olursa" dizileri için iyi).
• Formal doğrulama: en yüksek güvence için makine tarafından doğrulanmış ispatlar.

Ne kadar derine inilmeli?

Formalite derinliğini şu kriterlerle tartın:

• Risk: etki × olasılık. Yüksek risk daha güçlü garantileri hak eder.
• Maliyet: belirtme, ispat ve bakım zamanı.
• Değişim hızı: hızlı değişen kodu formal olarak sabitlemek zordur; önce arayüzleri sabitleyin.
• Ekip becerileri: eğer ispatlar teslimatı çok yavaşlatacaksa önce kontratlar ve statik analizle başlayın.

Pratikte "formalite"yi kademeli ekleyebileceğinizi de unutmayın: önce açık kontratlar ve invariantlar, sonra otomasyonla bunları sürdürün.

Koder.ai gibi araçlarla hızlı geliştirme yapan ekiplerde React ön yüzü, Go arka ucu ve Postgres şeması kısa döngülerde üretilebilir—snapshot/rollback ve kaynak kodu dışa aktarma bu yinelemeyi hızlandırırken kontratların test ve statik analizle CI'de korunmasını kolaylaştırır.

Pratik kontrol listesi

Planlama veya kod incelemede "daha fazla formalize etmeli miyiz?" kapısı için hızlı kontrol:

1. En kötü makul hata nedir ve kim zarar görür (kullanıcılar, operasyon, düzenleyiciler)?
2. Testler önemli uç durumları ve durumları gerçekçi şekilde kapsayabilir mi?
3. Mantık durumlu mu, eşzamanlı mı, yoksa invariant/sınır ağırlıklı mı?
4. Genel giriş noktaları için açık ön/son koşullar yazabilir miyiz?
5. Daha derin doğrulama yapabileceğimiz küçük bir çekirdek izole edebiliyor muyuz?
6. Burada en iyi getiriyi hangi araç sağlar: güçlü tipler, statik analiz, kontratlar, model kontrol, yoksa ispat mı?
7. Bir sonraki çeyrekte ne değişecek ve garantilerin bozulmasını nasıl önleriz?

Daha fazla okumak için: design-by-contract, özellik tabanlı testler, durum makineleri için model kontrol, diliniz için statik analizörler ve formal doğrulama araçlarına giriş materyalleri.