Biçimsel Yöntemler: Sadece İyi Mühendislik Pratiği mi? (2024)
(brooker.co.za)- Büyük ölçekli, dağıtık ve kritik düşük seviyeli sistemlerde biçimsel yöntemler, yalnızca doğruluk için ek bir süreç değil; zaman ve maliyeti azaltan bir mühendislik pratiği olarak görülmeli
- Yazılımda tasarım ve uygulama kolayca iç içe geçer; geç gelen tasarım düzeltmeleri doğrudan uygulamanın yeniden yapılmasına ve API değişiklik maliyetlerine yol açar
- Uygulamaya geçmeden önce davranışı ve arayüzleri somut biçimde gözden geçirmek, hata yoğunluğunu ve üretim sonrası sorunları azaltır; doğru tasarıma daha hızlı ulaşmayı sağlar
- Hızla değişen kullanıcı gereksinimleri ya da UI, dokümantasyon, fiyatlandırma mantığı gibi biçimselleştirmesi zor alanlarda, kapsamlı ön biçimsel tasarımın faydası azalabilir
- TLA+ ve P gibi araçlar, tasarım aşamasında optimizasyonları ve kısıtları gözden geçirerek doğruluk ile performans arasındaki ödünleşimleri azaltmak için de kullanılabilir
İyi bir mühendislik pratiği olarak biçimsel yöntemler
- Biçimsel yöntemler, iyi yazılım mühendisliği pratiklerinin önemli bir parçasıdır
- Özellikle büyük ölçekli sistemler, dağıtık sistemler ve kritik düşük seviyeli sistemlerle çalışan mühendisler için uygulanabilir değeri yüksektir
- Mühendisliğin nihayetinde zamanı ve maliyeti optimize etme faaliyeti olduğu varsayımından yola çıkar
- Performans, ölçeklenebilirlik, sürdürülebilirlik ve verimlilik de birlikte değerlendirilir
- Biçimsel yöntemler ucuz ya da kolay değildir ve her geliştirme biçimine iyi uymaz; ancak yalnızca maliyeti artırdığı yönündeki sezgi her zaman doğru değildir
Maliyeti azaltan iki yol
- İlki yeniden işi azaltmaktır
- Yazılımda, diğer mühendislik alanlarından farklı olarak tasarım ve inşa çoğu zaman aynı anda gerçekleşebilir
- Tasarım yeterince ilerlememiş olsa bile uygulamaya başlanabilir
- Bu değişkenlik yazılımın güçlü yanıdır; ancak tasarım yinelemelerini uygulama yinelemelerine dönüştürerek maliyeti büyütebilir
- İkincisi değişiklik maliyetini yönetmektir
- Bir API’nin ya da sistemin müşterileri oluştuğunda değişiklik çok daha pahalı ve zor hale gelir
- Hyrum’s Law uyarınca, yeterli sayıda API kullanıcısı olduğunda sözleşmede ne yazdığından bağımsız olarak gözlemlenebilir her davranışa birileri bağımlı hale gelir
- Sistem davranışını API ile yalıtmak, yazılım mühendisliğinin önemli fikirlerinden biridir; ancak kullanıcıların uygulama ayrıntılarına kadar bağımlı olabilmesi sınırlaması devam eder
- API’nin arkasındaki sistemi tamamen yeniden uygulamak mümkün olsa da soyutlama, değişiklik maliyetini ortadan kaldırmaz
- Biçimsel tasarım çalışması, yeniden iş maliyetini azaltır ve arayüz değişikliklerinin daha erken ele alınmasını sağlayarak yazılım geliştirme hızını ve verimliliğini artırabilir
Biçimsel tasarıma uygun sistemler
- Tüm yazılımlara aynı şekilde uygulanmaz
- Hızla evrilen ya da biçimselleştirmesi zor kullanıcı gereksinimlerinin çok olduğu yazılımlarda ön tasarımın değeri zayıflayabilir
- UI, web sitesi ve fiyatlandırma mantığı uygulamaları buna dahildir
- Bu alanlarda sürekli yeniden iş fazla olduğu için ön tasarım maliyeti büyüyebilir
- Agile’ın temel fikri, uygulamayı ve gereksinim toplamayı paralel yürüterek yayınlamaya kadar geçen süreyi kısaltmaktır
- Gereksinim toplama devam ederken bile uygulamanın tamamlanabilmesini sağlar
- Çoğu durumda bu paralel geliştirme biçimi ya en uygunudur ya da ilerlemeyi mümkün kılan zorunlu koşuldur
- Buna karşılık büyük ölçekli, dağıtık ve düşük seviyeli sistemlerin pek çok bölümünde gereksinimler iyi anlaşılmıştır
- En azından yeterince büyük bir statik gereksinim bölümü vardır
- Bu durumda ön biçimsel tasarım, uygulama aşamasındaki ve üretim sonrasındaki yeniden işi ve hata yoğunluğunu önemli ölçüde azaltabilir
- Gereksinimler fizik yasalarına ne kadar yakınsa tasarımın ve biçimsel tasarımın değeri o kadar artar; kullanıcı görüşlerine ne kadar yakınsa bu değer o kadar azalır
Gereksinim dokümantasyonu ve biçimselleştirmenin sınırları
- Kullanıcı gereksinimlerini açıkça yazmak, biçimsel olsun ya da olmasın çok değerlidir
- Gereksinimler yazılmazsa zaman boşa harcanır ve insanlar farklı yönlere hareket ederek sürtüşme yaratabilir
- Tüm insan gereksinimlerini biçimsel olarak belirtmek zor ya da ekonomik olmayabilir
- UI estetiği gereksinimleri
- Dokümantasyonun okunabilirliği
- API adlandırma tutarlılığı
- Biçimsel yaklaşıma ilişkin görüş ayrılıkları, biçimsel yaklaşımın ne olduğu ve hangi şekilde değer yarattığı konusundaki farklı düşüncelerden de kaynaklanır
- UML gibi kodu kapsamlı diyagramlara aktaran yöntemlerin, zor soruları doğrudan ele alamadığında değeri düşebilir
- Kötü yöntemlerle ya da kötü araçlarla yapıldığında değerli işler bile işe yaramaz hale gelebilir
Sahada yararlı biçimsel yöntemler ve araçlar
- Biçimsel yöntemler ve otomatik akıl yürütme geniş bir alandır ve çeşitli araçlar vardır
- Büyük bulut sistemleri alanında yararlı olmuş araç grupları şunlardır
- P, TLA+, Alloy gibi belirtim dilleri ve ilgili model denetleyicileri
- turmoil gibi deterministik simülasyon araçları
- Fuzzing ile birlikte, durum uzayını test yoluyla sistematik biçimde keşfetmek için kullanılır
- Dafny gibi doğrulamaya uygun programlama dilleri ve Kani gibi kod doğrulayıcıları
- Sayısal simülasyon teknikleri
- Beyaz tahta ya da tasarım dokümanlarında karar tabloları, doğruluk tabloları ve açık durum makineleri çizen biçimsele yakın yöntemler
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3, hafif biçimsel yöntemleri incelemek için bir başlangıç noktasıdır
- Tek hedef uygulama doğrulaması değildir
- TLA+ ve P gibi araçlar, uygulamadan önce tasarımı daha hızlı ve daha somut biçimde gözden geçirmede büyük değer taşır
Daha hızlı yazılımı daha hızlı yapmak
- 2015’te How Amazon Web Services Uses Formal Methods yazıldığı sırada odak çoğunlukla doğruluktu
- Tasarımın güvenlik ve canlılık özelliklerini doğrulamak
- Doğru tasarıma daha hızlı ulaşmak
- Dahili kilit yönetim sisteminde TLA+ kullanan ekibin örneğinde, “agresif optimizasyonları doğrulamak” önemli bir noktaydı
- TLA+ gibi araçlar yalnızca sistemleri daha hızlı yapmayı sağlamaz; daha hızlı sistemler yapmayı da sağlayabilir
- Olası optimizasyonları hızla keşfeder
- Gerçekten önemli kısıtları bulur
- Önerilen optimizasyonun doğru olup olmadığını kontrol eder
- Çoğu durumda biçimsel yöntemler, sistemlerin kolayca içine düşebileceği doğruluk ile performans arasındaki zor ödünleşimleri azaltır
Tasarım aşamasında kullanılan araçların değeri
- Sistem tasarımını düşünmeye yardımcı olan araçları tasarım aşamasında kullanmak, yazılım geliştirme hızını büyük ölçüde artırabilir
- Riski azaltır ve en baştan daha optimize edilmiş sistemler yapılmasını sağlar
- Büyük ölçekli ve karmaşık sistemler inşa eden mühendisler için biçimsel yöntemler, iyi mühendislik pratiklerinin bir parçasıdır
1 yorum
Hacker News yorumları
Yazılımda biçimsel doğrulama, yazıda da kabul edildiği gibi yazılımın türüne ve geliştirme sürecine büyük ölçüde bağlıdır.
Biçimsel doğrulama kullanmak için yazılım davranışına ilişkin biçimsel gereksinimler gerekir; oysa çoğu proje ve tasarım felsefesi buna uymaz. Ne istendiği bile kesin değilken geliştirme ile tasarım birlikte ilerliyorsa biçimsel yöntemleri uygulamak zordur. Ancak küçük ve güvenliğin kritik olduğu sistemler gibi önceden hazırlanmış belirtimlere dayanan alanlar büyük fayda görebilir; havacılık ve uzay yazılımları bunun tipik örneğidir.
Bugün bunlar doktora derecesi ya da yıllarca araştırma gerektiren beceriler değil; temel düzeyde yüksek seviyeli belirtim yazmak da öyle. Bir model denetleyici kullanınca, modellediğiniz sistem hakkında bir şeyler öğrenirsiniz; yalnızca dokümantasyon veya eğitim amacıyla kullanılsa bile faydalıdır. Biçimsel yöntemlerin temel gücü, insanı sonuna kadar düşünmeye zorlamasında yatar. Birçok geliştirici, kendi kafası, tip denetleyici ve biraz birim testiyle eşzamanlılık algoritmaları uygulayabileceğine inanır; ama bir model denetleyici çalıştırdıktan sonra tasarımda ve varsayımlarda hatalar bulunca ister istemez alçakgönüllü olur. Sanılandan daha çok küçük dağıtık sistem vardır ve durum uzayı, biçimselleştirip bakmadan önce tahmin edilenden çoğu zaman çok daha büyüktür.
Örneğin çok karmaşık bir durum makinesine özellik tabanlı testler ekleyerek, endpoint hangi tuhaf girdilerle çağrılırsa çağrılsın iç durum makinesinin geçersiz geçişler yapmadığını doğruladık. Etrafındaki kodun biçimsel belirtimi yoktu ama durum makinesinin vardı; bu sayede mümkün oldu ve geleneksel birim testlerinin asla yakalayamayacağı incelikli hatalar da bulduk.
Ancak biçimsel yöntemlerden fayda görmek için program davranışını programın kendisi olmayan başka bir şeyle karşılaştırmak gerekir; o başka şeyin de biçimsel bir dilde yazılmış olması gerekir. İstenen davranışı doğru anlamak gerekir, ama bunun yazılımın tüm davranışını kapsaması şart değildir. Otomatik birim testleri de biçimsel belirtimdir; bunları çalıştırmak da biçimsel bir doğrulama yöntemidir. Genel olarak biçimsel yöntemler dendiğinde kastedilenden daha zayıf bir belirtim ve daha zayıf bir doğrulamadan ibarettir; kavramsal ya da pratik açıdan belirgin bir nitelik farkı yoktur. Testin uygulanabildiği bir yazılıma daha zengin biçimsel belirtim yöntemlerinin de uygulanabilme olasılığı yüksektir; maliyet-fayda dengesini de test etmeyi öğrenir gibi deneme yanılmayla öğrenirsiniz.
Sonunda mesele, bunun “çevik” diye adlandırılması için ne kadar daha fazla para ve zaman harcayacağınızdır. Paradoksal biçimde, geleneksel gereksinim aşaması bu üç yöntem içinde en ucuz olanıdır; değişiklik maliyetinin en düşük olduğu anda, yani bir satır metni değiştirme aşamasında müşteriyle hızla yakınsama sağladığı için özgün çevik ruhuna da en iyi uyan yöntemdir.
Yine de hiçbir durumu atlamadığınızı ve sistem içinde çelişki olmadığını kontrol etmenin faydasını elde edebilirsiniz.
Biçimsel yöntemler hakkında “yazılım büyük ve karmaşıktır, doğru yapmak zordur; o halde biçimsel yöntemler” şeklindeki mantığı sık görüyorum.
Bir yandan bunun doğru olmasını isterdim. Akademik olarak öğrenilen yaklaşımlarda güçlü olduğum için kişisel olarak da işime yarar; pratikte de yazılım gerçekten karmaşık olduğu için başarısız olduğunda nedenini arayıp durmak sinir bozucu. Ama biçimsel yöntemlerin bu sorunu nasıl çözdüğünü ikna edici biçimde gösteren örnekler çok az. Bu yazı, modern “tasarım”ın büyük kısmının zaman kaybı olduğuna işaret etmesi bakımından daha iyi; fakat TLA’nın UML’den neden daha iyi olduğunu yeterince açıklamıyor. Sanki TLA’ya aylar ya da yıllar yatırınca bir aydınlanma yaşanacağı ve aydınlanmamış kişilere açıklanamayan bir biçimde faydalı olduğunun anlaşılacağı ima ediliyor gibi. Kalkülüs ya da Bayes istatistiğinde de böyle bir yön var, dolayısıyla imkânsız bir iddia değil; ama sonunda “gerçekten bu kadar faydalı olsaydı daha çok kişi kullanırdı ve avantajları kendiliğinden ortaya çıkardı” şeklindeki proje yöneticisi tipi yargıya geri dönüyorsunuz. Uzun zamandır var olup da yaygın biçimde yerleşmemişse, büyük olasılıkla bir nedeni vardır.
Düşünmesi zor bir problemle karşılaşınca bir tür “yöntem” kullanırsınız. Bir iletişim protokolüyse, bunu durum makinesiyle açıklamak iyidir; TLA da bu nişe daha iyi uyar. Son zamanlarda bu düzeyde çabayı haklı çıkaracak çok sorun yoktu, ama böyle bir sorun çıktığında değeri muazzam olur. Alana özgü diller de benzer: çeşitli sorunlardan kaçınmak için doğrudan parser yazmaktansa bir parser framework’ü kullanmak çok daha iyidir. Bugün yeniden işlerin çoğu, gereksinim değişikliklerinden ve müşterinin gerçekte ne istediğini bilmeden “bu değil” demesinden kaynaklanıyor. Talepte bulunanların kendi gereksinimlerinin sonuçlarını yeterince düşünmemesi de var; ama daha büyük sorun, iyi karar vermek için gereken bilginin tek bir yerde yeterince toplanmaması.
Biçimsel yöntemler kesinlikle büyük bir yatırım. Yine de genel olarak yerleşmemiş olsalar da, fikirlerinin bir kısmı modern tip sistemlerine girdi.
Edindiğim izlenim, biçimsel doğrulayıcının katılığının sırf makul süre ve bellek içinde bitmesi gerektiği için bile tasarım karmaşıklığına sınır koyduğu yönünde. Belki de biçimsel doğrulama istemenin asıl kazanımı, “yazılım büyük, karmaşık ve doğru yapmak zor” problemini, büyük karmaşık programlarla uğraşmayı can sıkıcı hale getirerek çözmesindedir.
SAT ya da TLA tekniklerini kullanarak girdi uzayını tekrarlanabilir biçimde hızla daraltan özellik tabanlı testlerin ardıllarını görmek isterim. Parsing ve kod kapsamı üzerinden, bir fonksiyona 12 vermenin 11’den farklı bir dala giremeyeceğini; ama -1 ya da 2^17 < n < 2^32 gibi değerlerin farklı olabileceğini çıkarabilmeli.
Yazılım projelerinin çoğu hâlâ başarısız oluyor. Bu bir “piyasa başarısızlığı” değil, daha çok düpedüz “üretmeyi başaramama” durumudur.
Biçimsel yöntemlerin kabaca iki kolu var: kodun kendisinden ayrı duran ve genellikle kodun belirtimini çıkarsayan dışsal yöntemler ile kodun içine girip kod hakkında daha doğrudan akıl yürüten içsel yöntemler.
Tarihsel olarak tip sistemleri gibi içsel yöntemler fonksiyon düzeyinde kod hakkında akıl yürütürken, Spin/P gibi karar verilebilir model denetleyicileri gibi dışsal yöntemler otomata benzeri biçimciliklerle tanımlanmış kod modelleriyle uğraştı. Şu an biçimsel yöntem araştırmalarının altın çağı olduğunu düşünüyorum; tip sistemlerindeki gelişmeler ve Verus gibi projelerin ileri ittiği içsel yöntemlere kıyasla dışsal yöntemlerin giderek daha az tercih edildiği bir akım var gibi görünüyor. https://github.com/verus-lang/verus
Rust gibi ayak izi büyük bir dilde bunun nasıl işleyeceğine dair sorular gördüm, ama henüz iyi bir yanıt görmedim. Daha fazla okumak isterim.
İçsel yöntemlerin ayrı bir belirtim yazıp sürdürmek gerekmediği için tercih edildiği söyleniyor gibi gelmişti, ama gerçekte öyle değil.
Hafif biçimsel yöntemlere değinilen kısım iyi. Kod tabanının yanında bir proptest stratejileri koleksiyonu tutmak, elle birim testleri yazmaktan çok daha büyük bir yatırım değil; ama geniş kapsam ve küçük, anlaşılır başarısızlık örnekleri sayesinde çok daha iyi içgörü sağlıyor.
Üstelik bu yaklaşım genel yazılım geliştirme pratikleriyle de iyi uyum sağlıyor. https://crates.io/crates/proptest
İyi test yazmanın yolunu ve bunun gerektirdiği emeği bir ölçüde biliyorum; ama LLM benden çok daha hızlı şekilde daha iyi testler üretebiliyor. Tekrarlı ve sıkıcı işler yaparken sabrı azalan bana kıyasla, aksine daha az baştan savma davranma ihtimali yüksek. Bir yazılım mühendisiyseniz, tekrarlı hissettiren işleri otomatikleştirmeye yönelik bir refleksiniz olmalı; dokümantasyon da artık üretilerek daha sık ve daha erken yapılıyor. LLM, biçimsel doğrulamanın benimsenmesinde küçük bir devrim yaratabilir. Doğru belirtim üretmek sıkıcıdır; ama çalışan kod, dokümantasyon ve ipuçları gibi yeterli bağlam varsa LLM için görece kolay bir iş olabilir. Belirtimi tamamen elle yazmaktansa ürettirip sonra gözden geçirebilmek, bunu yapma isteğini çok daha fazla artırır. Rust kullanmak, doğruluğu önemsediğinize dair bir işarettir; derleyicisi de biçimsel yöntemler olmadan sistemin muhtemelen doğru olduğunu kanıtlamaya en çok yaklaşan araçlardan biridir. Derleyicisi ya da açık tipleri bile olmayan bir dile biçimsel yöntemler eklemekten çok daha kolay olma olasılığı yüksektir.
Yazılımda biçimsel doğrulama, hâlâ uç örnekler dışında değer sağlayacak kadar kullanılması kolay değil. Buna karşılık donanımda biçimsel doğrulama kullanmamak için neredeyse hiçbir neden yok
Öğrenmeye çalışmayı sürdürüyorum ama çoğu sistemde “derleyiciyi bizzat yazmış kişi” düzeyinde uzman olmanız gerekiyor. Örneğin bir varint kodlayıcı/kod çözücüyü kanıtlamaya çalıştım; 1–2 bayt için oldu ama daha fazlasında olmadı. Yardım istediğimde, bunun derleyicinin içeride döngüyü yalnızca 5 kez açması gibi, bilmemin mümkün olmadığı iç ayrıntılardan kaynaklandığını öğrendim. Son zamanlarda Lean öğreniyorum; hoşuma gidiyor ama şöyle belgelerle karşılaşıyorum: “Definitional equality includes η-equivalence…” gibi. Lean’i kötülemek istemiyorum; aksine alternatifler arasında belgeleri daha iyi olanlardan biri gibi görünüyor
Biçimsel yöntemlerin illa karmaşık olması gerekmez. Sorun, çoğu biçimsel yöntemin bir profesörün ilgilendiği belirli bir konuyu göstermek için hazırlanmış akademik alıştırmalar gibi tasarlanmış olması. TLA+ da daha çok makale yazımı için tasarlanmış tarafa yakın
Hafif biçimsel yöntemler arasında çok bilinmeyen ama sevdiğim bir yaklaşım, doğrusal zaman mantığı kullanarak iz doğrulaması yapmak: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
Temelde yalnızca olayları loglamak yeterli; olay tabanlı mimarilerde bunu neredeyse bedavaya elde edebilirsiniz. Ardından yürütme izleri üzerinde
Always(Locked, Implies(Eventually(Unlocked)))gibi yüklemleri çalıştırırsınız. Geçmiş izlere de uygulanabilir; stres testleri veya fuzzing ile birleştirilerek durum uzayı keşfedilebilir. Basit, güçlü ve yaygın biçimde uygulanabilir; modele gerek yok, yalnızca yüklemler yeterliBiçimsel yöntemler, sistem davranışı hakkında kapsamlı bir gerekçelendirme ima eder. TLA veya benzeri sistemlerde, gerçek sistem değil bir durum makinesi olsa da, çıktı LTL/CTL/TLA özelliklerinin sistemin tüm davranışları, yani izler veya iz ağaçları için geçerli olduğunun kanıtıdır
Önceki tartışma Haziran 2024’te yapılmıştı: https://news.ycombinator.com/item?id=40753989
15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - Mayıs 2024, 1 yorum
Çok yavaş. Plan yapmak kısa sürede fosilleşmek demek; herhangi bir belge de çevik mahkemesinde aleyhte delil olarak kullanılabilir
Biçimsel yöntemler hakkında okuduğum yazıların çoğu, danışmanların potansiyel müşteri toplaması gibi hissettiriyor
Bunun kendisi sorun değil ama çalışanlara ya da iş arkadaşlarına eğitim paketi satın aldırırsanız veya beni işe alırsanız kötü, hatta sorumsuzca tehlikeli programlama alışkanlıklarınızı düzelteceğim dercesine, biçimsel yöntemler yoluyla aydınlanmaya ulaşmış gibi davranılması rahatsız edici. Biçimsel yöntemler gerçekten spesifikasyondan sapması mümkün olmayan yüksek kaliteli kod üretmeye başladığında tekrar konuşalım
Biçimsel spesifikasyonda genellikle o düzeyde ayrıntı belirtilmez; sistemin genel davranışı belirtilir. Bu yüzden tek bir spesifikasyon çoğu zaman ince farkları olan birçok programa karşılık gelir. Kodun belge olarak yetersiz kalmasının nedeni de budur. Neyin kasıtlı bir seçim, neyin tesadüfi bir seçim olduğunu bilemezsiniz. Kod, üst düzey gereksinimleri açıklamak için fazla somuttur. Buna karşılık programı bir spesifikasyona göre doğrulamak daha uygulanabilir görünüyor
Günümüzde biçimsel yöntem savunucularının bir kısmı, biçimsel yöntem kullanmayanları “tembel” ya da “aptal” görüyor ve kendilerinin “doğru şeyi yaptığı” ya da “karmaşık bir dili ustalıkla kullandığı” gerekçesiyle üstünlük iddia etmeye çalışıyor
Elbette herkes böyle değil; iyi insanlar da tanıyorum ama bazıları aslında tek numarası olan kişilere daha yakın. Son birkaç yılda öğrendikleri veya denedikleri başka biçimsel yöntem sistemlerini sorduğunuzda, “çok meşgul” oldukları için yeni bir şey öğrenemediklerini söylüyorlar. Son dönemde kullanımı daha kolay biçimsel yöntemler arasında, Python lehçesi kullanıp sözde kod gibi okunan FizzBee, daha kolay sözdizimine sahip Quint ve C# kullanıcılarına tanıdık gelecek sözdizimi olan P var. Bu yazının yazarı da biçimsel yöntemlerin kendi sorunlarının yalnızca yarısını çözdüğünü yazmıştı: https://brooker.co.za/blog/2022/06/02/formal.html
Ama orada sözü edilen sorunu, yeni bile olmayan PRISM zaten çözüyor. Brooker’ın etrafına bakmaya ya da öğrenmeye çalışmaması dışında bir şey değil