Tony Hoare'ın Hoare mantığı, Quicksort ve güvenlik düşüncesi üzerine çalışmaları, doğru yazılım yazma ve inceleme için pratik tekniklerin gelişmesini nasıl etkilediğini öğrenin.
İ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.
İ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.
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:
Ç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, ç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 makale, gerçek kod tabanlarında sıkça görülen birkaç Hoare fikrine odaklanır:
{P} C {Q} ile tanımlama yolu.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.
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.
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.
Hatalar genellikle ekipler ortadaki adımı atladığında olur: gereksinimden doğrudan koda atlanır ve "söz" bulanık kalır.
Sıkça karışan iki iddia vardır:
Gerçek sistemlerde, "hiç bitmemek" yanlış cevap vermek kadar zararlı olabilir.
Doğruluk ifadeleri evrensel değildir; şu tür varsayımlara dayanır:
Varsayımları açık etmek "makinemde çalışıyor" u başkalarının da akıl yürütebileceği bir şeye çevirir.
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ığı, 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}
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.
a + b tamsayı tipine sığaravg = (a + b) / 2avg matematiksel ortalamaya eşittirEğ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.
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.
Hoare mantığı küçük ifadelerden çok adımlı koda kadar ölçeklenir:
x = x + 1 sonrası x hakkında hangi gerçekler doğrudur?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ı.
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.
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.
Günlük kodun çoğu birkaç güvenilir şablonu kullanabilir.
İndeksleri güvenli aralıkta tutun.
0 <= i <= nlow <= left <= right <= highBu invariant türü aralık dışı erişimi önlemekte ve dizi akıl yürütmesini somutlaştırmakta iyidir.
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.
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.
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."Küçülen bir ölçü bulamıyorsanız, sonsuz döngü riski olabilir.
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:
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.
Birkaç konu çoğu hataya neden olur:
Hoare tarzı akıl yürütmede ispatınızı tipik olarak iki parçaya ayırırsınız:
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.
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.
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 <= pivotA[p+1..hi] içindeki her öğe >= pivotSö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.
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.
i sağa kadar koşar; partition yine de sonlanmalı ve mantıklı bir p döndürmelidir.j sola kadar koşar; aynı sonlanma kaygısı vardır.< vs <=) işaretçiler takılabilir. Hoare şeması ilerlemenin sürmesi için tutarlı bir kural gerektirir.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 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.
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.)
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.
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.
Testler ve ispat-tarzı akıl yürütme aynı hedefe—güvene—ulaşmak ister ama farklı yollar izler.
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).
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:
Spec size "doğru"nun ne olduğunu söyler; testler gerçeğin ona uyup uymadığını kontrol eder.
Ö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:
Bu özellikler esasen postcondition'ların yürütülebilir kontrolleridir.
Ölçeklenebilir hafif rutin:
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.
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.
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.
Ağır formal yöntemlere gerek yok; ekipler küçük, tekrarlanabilir uygulamalar benimseyerek hemen fayda sağlar:
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ı).
Güvenlik kontrollerinin bir maliyeti vardır—CPU zamanı, karmaşıklık veya bazen yanlış reddetme.
Güvenlik düşüncesi zerafeti kanıtlamaktan ziyade karşılanamayacak hata modlarını önlemeye odaklanır.
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.
Bir değişikliği okurken her önemli fonksiyonu küçük bir sözleşme gibi çerçevelemeye çalışın:
Basit bir gözlemci alışkanlığı: pre/post koşullar bir cümlede söylenemiyorsa, kod muhtemelen daha net bir yapıya ihtiyaç duyar.
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.
Aşağıdaki konularla ilgilenen kodu incelerken ekstra açık olun:
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?"
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.
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.
Hafiften ağır ağırlığa çeşitli seçenekler vardır ve sıkça en iyi sonuçlar bunların kombinasyonundan çıkar:
Formalite derinliğini şu kriterlerle tartı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.
Planlama veya kod incelemede "daha fazla formalize etmeli miyiz?" kapısı için hızlı kontrol:
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.
Doğruluk, programın üzerinde anlaşılan bir spesifikasyona uyması demektir: izin verilen her giriş ve ilgili sistem durumu için gerekli çıktıları ve yan etkileri üretir ve hata davranışlarını taahhüt edildiği gibi ele alır. “Çalışıyormuş gibi görünüyor” genellikle sadece birkaç örnek kontrol ettiğiniz anlamına gelir; tüm giriş uzayını veya sınır durumlarını kontrol etmezsiniz.
Gereksinimler: işin plain dildeki hedefidir ("listeyi görüntülemek için sırala").
Spesifikasyon: bu ihtiyacın kesin, kontrol edilebilir versiyonudur ("yeni bir liste döndürür; artan sırada sıralı, aynı çoklu küme elemanları, giriş değişmemiş").
Uygulama: yazdığınız koddur. Hatalar genellikle ekiplerin gereksinimden doğrudan koda atlaması ve kontrol edilebilir vaadi yazmamasıyla ortaya çıkar.
Kısmi doğruluk: kod dönerse, sonuç doğrudur.
Toplam doğruluk: kod döner ve sonuç doğrudur—yani sonlanma iddiasınındır.
Gerçekte, sonsuza kadar çalışmak kullanıcı görünür hatası, kaynak sızıntısı veya güvenlik riski olduğunda toplam doğruluk önemlidir.
Bir Hoare üçlüsü {P} C {Q}, basitçe bir sözleşme gibi okunur:
P (precondition): C çalıştırılmadan önce doğru olması gerekenlerPreconditions, kodun ihtiyacı olan şeylerdir (ör. "indeksler aralıkta", "elemanlar karşılaştırılabilir", "kilit elde"). Eğer bir ön koşul çağıranlar tarafından ihlal edilebilecekse ya:
Aksi takdirde son koşullar sadece temenni olur.
Bir döngü invarianti, 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. Yeniden kullanılabilecek şablonlar:
0 <= i <= n)Bir invariant ifade edemiyorsanız, döngü muhtemelen çok fazla işi aynı anda yapıyor veya sınırlar belirsizdir.
Genellikle her yinelemede azalan ve sonsuza dek azalması mümkün olmayan bir ölçü (variant) isimlendirirsiniz, örneğin:
n - i her seferinde 1 azalırAzalmayan bir ölçü bulamıyorsanız, gerçek bir sonlanmama riski keşfetmiş olabilirsiniz (özellikle çoğaltmalar veya takılı işaretçilerle).
Quicksort'ta partition, tüm algoritmanın dayandığı küçük ama kritik rutindir. Hatalı bir partition şunlara yol açabilir:
Bu yüzden partition sözleşmesini açıkça belirtmek faydalıdır: sol tarafta ne doğru olmalı, sağ tarafta ne olmalı ve elemanların yalnızca yeniden düzenlendiği (permutasyon) garanti edilmeli.
Çoğaltmalar ve pivot ile “eşit” elemanların ele alınışı sık görülen hata noktalarıdır. Pratik kurallar:
Eğer çoğaltmalar sıksa, hem hataları hem özyineleme derinliğini azaltmak için üç-yollu partition düşünülebilir.
Testler somut hataları yakalar; akıl yürütme belirli hata sınıflarını ortadan kaldırabilir. Pratik yaklaşım:
Sıralama için iki yüksek faydalı özellik:
C: kod parçasıQ (postcondition): C bitince doğru olacaklar, varsayım P geçerliyseKötü amaç, notasyonu koda yazmak değildir; incelemelerde “girilen varsayımlar, çıkan garantiler” yapısını kullanmak pratik kazançtır.