Bu makale bir çeviridir . Ama ondan önce küçük bir giriş. Zombiler nasıl oluşur? Herkes bir arkadaşını veya meslektaşını kendi seviyesine çekmek istediği bir duruma girdi ama olmuyor. Ve onunla olduğu kadar seninle de "işe yaramıyor": ölçeğin bir tarafında normal bir maaş, görevler vb. Ve diğer tarafında düşünme ihtiyacı var. Düşünmek tatsız ve acı vericidir. Çabucak pes eder ve beynini hiç açmadan kod yazmaya devam eder. Öğrenilmiş çaresizlik engelini aşmanın ne kadar çaba gerektirdiğini hayal edersiniz ve bunu yapmazsınız. Görünüşe göre iyileştirilebilen zombiler bu şekilde oluşuyor, ancak görünüşe göre kimse bunu yapmayacak.
Bunu gördüğümde (evet, ders kitaplarından aynı yoldaş) ve rapor yapmıyor ama soru cevap şeklinde biraz temkinliydim. Her ihtimale karşı, Leslie dünyaca ünlü bir bilim adamıdır, dağıtılmış hesaplamadaki temel çalışmaların yazarıdır ve onu LaTeX - “Lampport TeX” kelimesindeki La harflerinden de tanıyabilirsiniz. İkinci endişe verici faktör, onun gerekliliğidir: gelen herkes (kesinlikle ücretsiz olarak) birkaç raporunu önceden dinlemeli, bunlarla ilgili en az bir soru bulmalı ve ancak o zaman gelmelidir. Lamport'un orada ne yayınladığını görmeye karar verdim - ve bu harika! Tam olarak o şey, zombileri iyileştirmek için sihirli bağlantı hapı. Sizi uyarıyorum: metinden, süper esnek metodolojileri sevenler ve yazılanları test etmekten hoşlanmayanlar, özellikle yanabilir.
Habrokattan sonra aslında seminerin çevirisi başlıyor. Okumanın tadını çıkar!
Hangi görevi üstlenirseniz üstlenin, her zaman üç adımdan geçmeniz gerekir:
- hangi hedefe ulaşmak istediğinize karar verin;
- hedefinize nasıl ulaşacağınıza karar verin;
- hedefine gel
Bu aynı zamanda programlama için de geçerlidir. Kod yazarken şunları yapmalıyız:
- programın ne yapması gerektiğine karar verin;
- görevini nasıl yapması gerektiğini belirlemek;
- ilgili kodu yazınız.
Son adım elbette çok önemli ama bugün bundan bahsetmeyeceğim. Bunun yerine, ilk ikisini tartışacağız. Her programcı çalışmaya başlamadan önce bunları gerçekleştirir. Bir tarayıcı mı yoksa bir veritabanı mı yazdığınıza karar vermediğiniz sürece yazmak için oturmazsınız. Hedef hakkında belirli bir fikir mevcut olmalıdır. Ve kesinlikle programın tam olarak ne yapacağını düşünürsünüz ve kodun bir şekilde bir tarayıcıya dönüşeceği umuduyla bir şekilde yazmazsınız.
Bu kod ön düşünmesi tam olarak nasıl gerçekleşir? Bunun için ne kadar çaba sarf etmeliyiz? Her şey, çözdüğümüz sorunun ne kadar karmaşık olduğuna bağlı. Hataya dayanıklı dağıtılmış bir sistem yazmak istediğimizi varsayalım. Bu durumda, kodlamaya başlamadan önce her şeyi dikkatlice düşünmeliyiz. Ya bir tamsayı değişkenini 1 artırmamız gerekirse? İlk bakışta burada her şey önemsiz ve düşünmeye gerek yok ama sonra bir taşmanın olabileceğini hatırlıyoruz. Bu nedenle, bir sorunun basit mi yoksa karmaşık mı olduğunu anlamak için bile önce düşünmek gerekir.
Sorunun olası çözümlerini önceden düşünürseniz, hatalardan kaçınabilirsiniz. Ancak bu, düşüncenizin net olmasını gerektirir. Bunu başarmak için düşüncelerinizi yazmanız gerekir. Dick Guindon'ın şu sözünü gerçekten çok seviyorum: "Yazdığınızda, doğa size düşüncelerinizin ne kadar baştan savma olduğunu gösterir." Yazmazsanız, yalnızca düşündüğünüzü düşünürsünüz. Ve düşüncelerinizi özellikler şeklinde yazmanız gerekir.
Spesifikasyonlar, özellikle büyük projelerde birçok işlevi yerine getirir. Ama sadece bir tanesinden bahsedeceğim: net düşünmemize yardımcı oluyorlar. Açıkça düşünmek çok önemli ve oldukça zor, bu yüzden burada herhangi bir yardıma ihtiyacımız var. Spesifikasyonları hangi dilde yazmalıyız? Genel olarak, bu her zaman programcılar için ilk sorudur: hangi dilde yazacağız. Bunun tek bir doğru cevabı yok: çözdüğümüz problemler çok çeşitli. Bazıları için TLA+ benim geliştirdiğim bir özellik dilidir. Diğerleri için Çince kullanmak daha uygundur. Her şey duruma bağlıdır.
Daha da önemlisi başka bir soru: daha net düşünmeye nasıl ulaşılır? Cevap: Bilim adamları gibi düşünmeliyiz. Bu, son 500 yılda kendini kanıtlamış bir düşünce tarzıdır. Bilimde, gerçekliğin matematiksel modellerini inşa ederiz. Astronomi belki de kelimenin tam anlamıyla ilk bilimdi. Astronomide kullanılan matematiksel modelde gök cisimleri, gerçekte dağlar ve okyanuslar, gelgitler ve gelgitler ile son derece karmaşık nesneler olmalarına rağmen, kütle, konum ve momentuma sahip noktalar olarak görünürler. Bu model, diğerleri gibi, belirli sorunları çözmek için yaratılmıştır. Bir gezegen bulmanız gerektiğinde teleskopu nereye doğrultacağınızı belirlemek için harikadır. Ancak bu gezegendeki hava durumunu tahmin etmek istiyorsanız, bu model çalışmaz.
Matematik, modelin özelliklerini belirlememizi sağlar. Ve bilim, bu özelliklerin gerçeklikle nasıl ilişkili olduğunu gösterir. Bilimimizden, bilgisayar biliminden bahsedelim. Çalıştığımız gerçeklik, çeşitli türden bilgi işlem sistemleridir: işlemciler, oyun konsolları, bilgisayarlar, yürütme programları vb. Bilgisayarda bir program çalıştırmaktan bahsedeceğim, ancak genel olarak tüm bu sonuçlar herhangi bir bilgi işlem sistemi için geçerlidir. Bilimimizde birçok farklı model kullanıyoruz: Turing makinesi, kısmen sıralı olaylar dizisi ve diğerleri.
program nedir? Bu, bağımsız olarak kabul edilebilecek herhangi bir koddur. Bir tarayıcı yazmamız gerektiğini varsayalım. Üç görevi yerine getiriyoruz: kullanıcının programa bakışını tasarlıyoruz, ardından programın üst düzey diyagramını yazıyoruz ve son olarak kodu yazıyoruz. Kodu yazarken bir metin biçimlendirici yazmamız gerektiğini fark ediyoruz. Burada yine üç sorunu çözmemiz gerekiyor: bu aracın hangi metni döndüreceğini belirleyin; biçimlendirme için bir algoritma seçin; kod yaz Bu görevin kendi alt görevi vardır: sözcüklere doğru bir şekilde kısa çizgi ekleyin. Bu alt görevi de üç adımda çözüyoruz - görebileceğiniz gibi, bunlar birçok düzeyde tekrarlanıyor.
İlk adımı daha ayrıntılı olarak ele alalım: programın hangi sorunu çözdüğü. Burada, genellikle bir programı bir miktar girdi alan ve bir miktar çıktı üreten bir fonksiyon olarak modelliyoruz. Matematikte, bir fonksiyon genellikle sıralı bir çiftler kümesi olarak tanımlanır. Örneğin, doğal sayılar için kare alma işlevi {<0,0>, <1,1>, <2,4>, <3,9>, …} kümesi olarak tanımlanır. Böyle bir fonksiyonun alanı, her çiftin ilk elemanlarının, yani doğal sayıların kümesidir. Bir işlevi tanımlamak için kapsamını ve formülünü belirtmemiz gerekir.
Ancak matematikteki işlevler, programlama dillerindeki işlevlerle aynı değildir. Matematik çok daha kolay. Karmaşık örneklere ayıracak vaktim olmadığı için basit bir tanesini ele alalım: C'deki bir işlev veya Java'daki iki tamsayının en büyük ortak bölenini döndüren statik bir yöntem. Bu yöntemin belirtiminde şunu yazacağız: hesaplar GCD(M,N) argümanlar için M и NNerede GCD(M,N) - etki alanı tamsayı çiftleri kümesi olan ve dönüş değeri şuna bölünebilen en büyük tamsayı olan bir işlev: M и N. Bu model gerçeklikle nasıl ilişkilidir? Model tamsayılar üzerinde çalışırken, C veya Java'da 32-bit'e sahibiz. int. Bu model, algoritmanın doğru olup olmadığına karar vermemizi sağlar. GCD, ancak taşma hatalarını engellemez. Bu, zamanın olmadığı daha karmaşık bir model gerektirecektir.
Model olarak bir fonksiyonun sınırlamalarından bahsedelim. Bazı programlar (işletim sistemleri gibi) sadece belirli argümanlar için belirli bir değer döndürmez, sürekli olarak çalışabilirler. Ek olarak, model işlevi ikinci adım için pek uygun değildir: sorunun nasıl çözüleceğini planlamak. Hızlı sıralama ve kabarcık sıralama aynı işlevi hesaplar, ancak bunlar tamamen farklı algoritmalardır. Bu nedenle, programın amacına nasıl ulaşıldığını anlatmak için farklı bir model kullanıyorum, buna standart davranış modeli diyelim. İçindeki program, her biri sırayla bir durum dizisi olan izin verilen tüm davranışların bir kümesi olarak temsil edilir ve durum, değerlerin değişkenlere atanmasıdır.
Öklid algoritmasının ikinci adımının nasıl olacağını görelim. hesaplamamız gerekiyor GCD(M, N). Başlatıyoruz M gibi xVe N gibi y, ardından eşit olana kadar bu değişkenlerden küçük olanı büyük olandan tekrar tekrar çıkarın. Örneğin, eğer M = 12Ve N = 18, aşağıdaki davranışı tanımlayabiliriz:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ve eğer M = 0 и N = 0? Sıfır tüm sayılara bölünebilir, bu nedenle bu durumda en büyük bölen yoktur. Bu durumda ilk adıma geri dönüp şunu sormalıyız: Pozitif olmayan sayılar için gerçekten OBEB hesaplamamız gerekiyor mu? Bu gerekli değilse, sadece spesifikasyonu değiştirmeniz gerekir.
Burada üretkenlik hakkında küçük bir inceleme yapmalıyız. Genellikle günde yazılan kod satırı sayısıyla ölçülür. Ancak belirli sayıda satırdan kurtulursanız işiniz çok daha kullanışlıdır çünkü böcekler için daha az yeriniz olur. Ve koddan kurtulmanın en kolay yolu ilk adımda. Uygulamaya çalıştığınız tüm zillere ve ıslıklara ihtiyacınız olmaması tamamen mümkündür. Bir programı basitleştirmenin ve zamandan tasarruf etmenin en hızlı yolu, yapılmaması gereken şeyleri yapmamaktır. İkinci adım, en çok zaman kazandıran ikinci potansiyeldir. Üretkenliği yazılan satırlarla ölçüyorsanız, bir görevi nasıl başaracağınızı düşünmek sizi daha az üretken, çünkü aynı sorunu daha az kodla çözebilirsiniz. Burada kesin istatistikler veremiyorum çünkü şartname üzerinde, yani birinci ve ikinci adımlarda zaman harcadığım için yazmadığım satır sayısını saymanın bir yolu yok. Ve deney burada da kurulamaz, çünkü deneyde ilk adımı tamamlama hakkımız yoktur, görev önceden belirlenmiştir.
Gayri resmi şartnamelerdeki birçok zorluğu gözden kaçırmak kolaydır. Fonksiyonlar için katı spesifikasyonlar yazmanın zor bir yanı yoktur, bunu tartışmayacağım. Bunun yerine, standart davranışlar için güçlü özellikler yazmaktan bahsedeceğiz. Herhangi bir davranış kümesinin güvenlik özelliği kullanılarak tanımlanabileceğini söyleyen bir teorem vardır. (Emniyet) ve hayatta kalma özellikleri (canlılık). Güvenlik, kötü bir şey olmayacağı anlamına gelir, program yanlış bir cevap vermez. Hayatta kalma, er ya da geç iyi bir şey olacağı anlamına gelir, yani program er ya da geç doğru cevabı verecektir. Kural olarak, güvenlik daha önemli bir göstergedir, hatalar en sık burada meydana gelir. Bu nedenle, zaman kazanmak için, elbette önemli olmasına rağmen, hayatta kalma hakkında konuşmayacağım.
İlk önce olası başlangıç durumları kümesini belirleyerek güvenliği sağlarız. İkincisi, her durum için sonraki tüm olası durumlarla olan ilişkiler. Bilim adamları gibi davranalım ve durumları matematiksel olarak tanımlayalım. İlk durumlar kümesi, örneğin Öklid algoritması durumunda bir formülle tanımlanır: (x = M) ∧ (y = N). Belirli değerler için M и N yalnızca bir başlangıç durumu vardır. Bir sonraki durumla olan ilişki, bir sonraki durumun değişkenlerinin bir asal ile yazıldığı ve mevcut durumun değişkenlerinin bir asal olmadan yazıldığı bir formülle tanımlanır. Öklid'in algoritması durumunda, iki formülün ayrışmasıyla ilgileneceğiz, bunlardan birinde x en büyük değerdir ve ikinci - y:
İlk durumda, y'nin yeni değeri, y'nin önceki değerine eşittir ve x'in yeni değerini, büyük olandan küçük değişkeni çıkararak elde ederiz. İkinci durumda, tersini yaparız.
Öklid'in algoritmasına geri dönelim. Tekrar varsayalım ki M = 12, N = 18. Bu, tek bir başlangıç durumunu tanımlar, (x = 12) ∧ (y = 18). Daha sonra bu değerleri yukarıdaki formüle yerleştirip şunu elde ederiz:
İşte olası tek çözüm: x' = 18 - 12 ∧ y' = 12ve davranışı elde ederiz: [x = 12, y = 18]. Benzer şekilde, davranışımızdaki tüm durumları şöyle tanımlayabiliriz: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
son durumda [x = 6, y = 6] ifadenin her iki kısmı da yanlış olacaktır, dolayısıyla sonraki durumu yoktur. Böylece, ikinci adımın tam bir tanımlamasına sahibiz - gördüğünüz gibi, bu, mühendisler ve bilim adamlarında olduğu gibi oldukça sıradan bir matematik ve bilgisayar bilimlerinde olduğu gibi garip değil.
Bu iki formül, zamansal mantığın tek bir formülünde birleştirilebilir. O zarif ve anlatması kolay ama şimdi ona ayıracak zaman yok. Zamansal mantığa sadece canlılık özelliği için ihtiyaç duyabiliriz, güvenlik için gerekli değildir. Zamansal mantığı bu şekilde sevmiyorum, pek sıradan bir matematik değil ama canlılık söz konusu olduğunda bu gerekli bir kötülük.
Euclid'in algoritmasında, her değer için x и y benzersiz değerlere sahip olmak x' и y', sonraki durumla ilişkiyi doğru yapan. Başka bir deyişle, Öklid'in algoritması deterministiktir. Deterministik olmayan bir algoritmayı modellemek için, mevcut durumun birden fazla olası gelecek durumuna sahip olması ve her bir asallaştırılmamış değişken değerinin, bir sonraki durumla ilişkinin doğru olması için birden fazla astarlanmış değişken değerine sahip olması gerekir. Bunu yapmak kolaydır, ancak şimdi örnek vermeyeceğim.
Çalışan bir araç yapmak için resmi matematiğe ihtiyacınız var. Şartname nasıl resmi hale getirilir? Bunu yapmak için resmi bir dile ihtiyacımız var, örneğin, . Öklid algoritmasının belirtimi bu dilde şöyle görünecektir:
Üçgen içeren eşittir işareti simgesi, işaretin solundaki değerin, işaretin sağındaki değere eşit olarak tanımlandığı anlamına gelir. Özünde, belirtim bir tanımdır, bizim durumumuzda iki tanımdır. TLA+'daki belirtime, yukarıdaki slaytta olduğu gibi bildirimler ve bazı sözdizimi eklemeniz gerekir. ASCII'de şöyle görünürdü:
Gördüğünüz gibi, karmaşık bir şey yok. TLA+ spesifikasyonu test edilebilir, yani küçük bir modeldeki tüm olası davranışları atlayabilir. Bizim durumumuzda, bu model belirli değerler olacaktır. M и N. Bu, tamamen otomatik olan çok verimli ve basit bir doğrulama yöntemidir. Resmi doğruluk kanıtları yazmak ve bunları mekanik olarak kontrol etmek de mümkündür, ancak bu çok zaman alır, bu nedenle neredeyse hiç kimse bunu yapmaz.
TLA+'nın ana dezavantajı, matematik olması ve programcıların ve bilgisayar bilimcilerinin matematikten korkmasıdır. İlk bakışta bu şaka gibi geliyor ama ne yazık ki bunu tüm ciddiyetimle söylüyorum. Meslektaşım bana TLA+'yı birkaç geliştiriciye nasıl açıklamaya çalıştığını anlatıyordu. Formüller ekranda belirir belirmez hemen cam gibi gözler oldular. TLA+ sizi korkutuyorsa, kullanabilirsiniz , bir tür oyuncak programlama dili. PlusCal'daki bir ifade, herhangi bir TLA+ ifadesi, yani genel olarak herhangi bir matematiksel ifade olabilir. Ayrıca PlusCal, deterministik olmayan algoritmalar için bir sözdizimine sahiptir. PlusCal, herhangi bir TLA+ ifadesini yazabildiği için, PlusCal herhangi bir gerçek programlama dilinden çok daha ifadelidir. Daha sonra, PlusCal kolayca okunabilen bir TLA+ özelliğinde derlenir. Bu, elbette, karmaşık PlusCal spesifikasyonunun TLA + 'da basit bir spesifikasyona dönüşeceği anlamına gelmez - sadece aralarındaki yazışma açıktır, ek bir karmaşıklık olmayacaktır. Son olarak, bu belirtim TLA+ araçlarıyla doğrulanabilir. Sonuç olarak, PlusCal matematik fobisinin üstesinden gelmeye yardımcı olabilir ve programcılar ve bilgisayar bilimcileri için bile anlaşılması kolaydır. Geçmişte, bir süre (yaklaşık 10 yıl) üzerine algoritmalar yayınladım.
Belki birisi TLA + ve PlusCal'ın matematik olduğuna ve matematiğin yalnızca icat edilmiş örnekler üzerinde çalıştığına itiraz edecektir. Uygulamada, türleri, prosedürleri, nesneleri vb. olan gerçek bir dile ihtiyacınız var. Bu yanlış. Amazon'da çalışan Chris Newcomb şöyle yazıyor: "TLA+'yı on büyük projede kullandık ve her durumda, onu kullanmak geliştirmede önemli bir fark yarattı çünkü üretime geçmeden önce tehlikeli hataları yakalayabildik ve bize ihtiyaç duyduğumuz içgörü ve güveni verdi. programın gerçekliğini etkilemeden agresif performans optimizasyonları yapın". Resmi yöntemleri kullanırken verimsiz kod elde ettiğimizi sık sık duyabilirsiniz - pratikte her şey tam tersidir. Ek olarak, programcılar yararlı olduklarından emin olsalar bile yöneticilerin resmi yöntemlere ihtiyaç duyulduğuna ikna edilemeyeceği görüşü vardır. Ve Newcomb şöyle yazıyor: “Yöneticiler artık TLA+ için spesifikasyonlar yazmak ve bunun için özel olarak zaman ayırmak için çok çalışıyorlar”. Yöneticiler, TLA+'nın işe yaradığını gördüklerinde bunu memnuniyetle kabul ederler. Chris Newcomb bunu yaklaşık altı ay önce yazdı (Ekim 2014), ama şimdi bildiğim kadarıyla TLA+ 14 değil 10 projede kullanılıyor. Başka bir örnek de XBox 360'ın tasarımında. Charles Thacker'a bir stajyer geldi ve bellek sistemi için şartname yazdı. Bu belirtim sayesinde, normalde fark edilmeyecek ve bu nedenle her XBox 360'ın dört saatlik kullanımdan sonra çökeceği bir hata bulundu. IBM mühendisleri, testlerinin bu hatayı bulmayacağını doğruladı.
İnternette TLA + hakkında daha fazla bilgi edinebilirsiniz, ancak şimdi resmi olmayan özellikler hakkında konuşalım. Nadiren en küçük ortak böleni ve benzerlerini hesaplayan programlar yazmak zorunda kalıyoruz. TLA+ için yazdığım güzel yazıcı aracı gibi programları çok daha sık yazıyoruz. En basit işlemden sonra, TLA + kodu şöyle görünür:
Ancak yukarıdaki örnekte, kullanıcı büyük olasılıkla bağlaç ve eşittir işaretlerinin hizalanmasını istemiştir. Dolayısıyla, doğru biçimlendirme daha çok şuna benzer:
Başka bir örneği ele alalım:
Burada ise tam tersine eşitler, toplama ve çarpma işaretlerinin kaynakta dizilimi rastgele olduğu için en basit işleme bile yetiyor. Genel olarak, doğru biçimlendirmenin kesin bir matematiksel tanımı yoktur, çünkü bu durumda "doğru", "kullanıcının ne istediği" anlamına gelir ve bu matematiksel olarak belirlenemez.
Gerçeğin bir tanımına sahip değilsek, o zaman tanımlamanın faydasız olduğu görülüyor. Ama değil. Bir programın ne yapması gerektiğini bilmememiz, onun nasıl çalıştığını düşünmemize gerek olmadığı anlamına gelmez, tam tersine, onun için daha fazla çaba sarf etmemiz gerekir. Spesifikasyon burada özellikle önemlidir. Yapılandırılmış baskı için en uygun programı belirlemek imkansızdır, ancak bu, onu hiç almamamız gerektiği anlamına gelmez ve bir bilinç akışı olarak kod yazmak iyi bir şey değildir. Sonunda, tanımları olan altı kuraldan oluşan bir belirtim yazdım. yorum şeklinde bir java dosyasında. İşte kurallardan birine bir örnek: a left-comment token is LeftComment aligned with its covering token. Bu kural, diyelim ki, matematiksel İngilizce ile yazılmıştır: LeftComment aligned, left-comment и covering token - tanımları olan terimler. Matematikçiler matematiği böyle tanımlarlar: terimlerin tanımlarını ve bunlara dayalı olarak kuralları yazarlar. Böyle bir belirtimin yararı, altı kuralın anlaşılmasının ve hata ayıklamanın 850 satır koddan çok daha kolay olmasıdır. Bu kuralları yazmanın kolay olmadığını söylemeliyim, hatalarını ayıklamak epey zaman aldı. Özellikle bu amaçla hangi kuralın kullanıldığını bildiren bir kod yazdım. Bu altı kuralı birkaç örnek üzerinde test ettiğim için 850 kod satırında hata ayıklamak zorunda kalmadım ve hataları bulmanın oldukça kolay olduğu ortaya çıktı. Java bunun için harika araçlara sahiptir. Kodu yeni yazmış olsaydım, çok daha uzun sürerdi ve biçimlendirme daha düşük kalitede olurdu.
Resmi bir belirtim neden kullanılamıyor? Bir yandan, doğru uygulama burada çok önemli değil. Yapısal çıktılar kesinlikle kimseyi memnun etmeyecek, bu yüzden tüm garip durumlarda doğru çalışmasını sağlamak zorunda değildim. Daha da önemlisi, yeterli alete sahip olmamamdı. TLA+ model denetleyicisi burada işe yaramaz, bu yüzden örnekleri manuel olarak yazmam gerekir.
Yukarıdaki spesifikasyon, tüm spesifikasyonlarda ortak olan özelliklere sahiptir. Koddan daha yüksek seviyededir. Herhangi bir dilde uygulanabilir. Herhangi bir araç veya yöntem onu yazmak için işe yaramaz. Hiçbir programlama kursu bu belirtimi yazmanıza yardımcı olmaz. Ve TLA+'da yapılandırılmış baskı programları yazmak için özel olarak bir dil yazmıyorsanız, bu belirtimi gereksiz kılabilecek hiçbir araç yoktur. Son olarak, bu belirtim kodu tam olarak nasıl yazacağımız hakkında bir şey söylemez, yalnızca kodun ne yaptığını belirtir. Kodu düşünmeye başlamadan önce sorunu düşünmemize yardımcı olması için belirtimi yazarız.
Ancak bu spesifikasyon, onu diğer spesifikasyonlardan ayıran özelliklere de sahiptir. Diğer özelliklerin %95'i önemli ölçüde daha kısa ve basittir:
Ayrıca, bu belirtim bir kurallar dizisidir. Kural olarak, bu zayıf spesifikasyonun bir işaretidir. Bir dizi kuralın sonuçlarını anlamak oldukça zordur, bu yüzden hata ayıklamak için çok zaman harcamak zorunda kaldım. Ancak bu durumda daha iyi bir yol bulamadım.
Sürekli çalışan programlar hakkında birkaç söz söylemeye değer. Kural olarak, örneğin işletim sistemleri veya dağıtılmış sistemler gibi paralel olarak çalışırlar. Çok az insan onları zihinsel olarak veya kağıt üzerinde anlayabilir ve bir zamanlar yapabilmiş olmama rağmen ben onlardan biri değilim. Bu nedenle, işimizi kontrol edecek araçlara ihtiyacımız var - örneğin, TLA + veya PlusCal.
Kodun tam olarak ne yapması gerektiğini zaten biliyorsam, bir belirtim yazmak neden gerekliydi? Aslında, sadece bildiğimi sanıyordum. Ek olarak, bir şartname ile, dışarıdan birinin tam olarak ne yaptığını anlamak için artık koda girmesine gerek yoktur. Bir kuralım var: genel kurallar olmamalı. Bu kuralın bir istisnası var elbette, izlediğim tek genel kural bu: Kodun ne yaptığının belirtilmesi, insanlara kodu kullanırken bilmeleri gereken her şeyi anlatmalıdır.
Peki programcıların düşünme hakkında tam olarak neyi bilmesi gerekiyor? Yeni başlayanlar için, herkesle aynı: eğer yazmıyorsanız, o zaman size sadece düşünüyormuşsunuz gibi görünür. Ayrıca, kodlamadan önce düşünmeniz gerekir, bu da kodlamadan önce yazmanız gerektiği anlamına gelir. Spesifikasyon, kodlamaya başlamadan önce yazdığımız şeydir. Herkes tarafından kullanılabilen veya değiştirilebilen herhangi bir kod için bir belirtim gereklidir. Ve bu "birisi", yazıldıktan bir ay sonra kodun yazarı olabilir. Büyük programlar ve sistemler, sınıflar, yöntemler ve hatta bazen tek bir yöntemin karmaşık bölümleri için bir belirtim gerekir. Kod hakkında tam olarak ne yazılmalıdır? Ne yaptığını, yani bu kodu kullanan herhangi bir kişi için neyin yararlı olabileceğini açıklamanız gerekir. Bazen kodun amacına nasıl ulaştığını belirtmek de gerekebilir. Algoritma sürecinde bu yöntemden geçtiysek, buna algoritma diyoruz. Daha özel ve yeni bir şeyse, buna üst düzey tasarım diyoruz. Burada resmi bir fark yoktur: her ikisi de bir programın soyut modelidir.
Bir kod belirtimini tam olarak nasıl yazmalısınız? Ana şey: kodun kendisinden bir seviye daha yüksek olmalıdır. Durumları ve davranışları tanımlamalıdır. Görevin gerektirdiği kadar katı olmalıdır. Bir görevin nasıl uygulanacağına dair bir belirtim yazıyorsanız, bunu sözde kodda veya PlusCal ile yazabilirsiniz. Resmi şartnameler üzerine spesifikasyonların nasıl yazılacağını öğrenmeniz gerekir. Bu size gayri resmi olanlarda da yardımcı olacak gerekli becerileri verecektir. Resmi şartname yazmayı nasıl öğrenirsiniz? Programlamayı öğrendiğimizde programlar yazdık ve sonra hatalarını ayıkladık. Burada da aynı: özellikleri yazın, model denetleyiciyle kontrol edin ve hataları düzeltin. TLA+ resmi bir belirtim için en iyi dil olmayabilir ve özel ihtiyaçlarınız için başka bir dil muhtemelen daha iyi olacaktır. TLA+'nın avantajı, matematiksel düşünmeyi çok iyi öğretmesidir.
Spesifikasyon ve kod nasıl bağlanır? Matematiksel kavramları ve uygulamalarını birbirine bağlayan yorumların yardımıyla. Grafiklerle çalışıyorsanız, program düzeyinde düğüm dizilerine ve bağlantı dizilerine sahip olacaksınız. Bu nedenle, grafiğin bu programlama yapıları tarafından tam olarak nasıl uygulandığını yazmanız gerekir.
Yukarıdakilerin hiçbirinin gerçek kod yazma işlemi için geçerli olmadığına dikkat edilmelidir. Kodu yazarken yani üçüncü adımı gerçekleştirdiğinizde, program üzerinden de düşünmeniz ve düşünmeniz gerekiyor. Bir alt görevin karmaşık veya belirsiz olduğu ortaya çıkarsa, onun için bir belirtim yazmanız gerekir. Ama burada kodun kendisinden bahsetmiyorum. Herhangi bir programlama dilini, herhangi bir metodolojiyi kullanabilirsiniz, bu onlarla ilgili değil. Ayrıca, yukarıdakilerin hiçbiri kodu test etme ve hata ayıklama ihtiyacını ortadan kaldırmaz. Soyut model doğru yazılmış olsa bile uygulanmasında hatalar olabilir.
Spesifikasyonların yazılması, kodlama sürecinde ek bir adımdır. Bu sayede birçok hata daha az çabayla yakalanabilir - bunu Amazon'daki programcıların deneyimlerinden biliyoruz. Spesifikasyonlarla, programların kalitesi yükselir. Öyleyse neden bu kadar sık onlarsız gidiyoruz? Çünkü yazmak zordur. Ve yazmak zordur çünkü bunun için düşünmeniz gerekir ve düşünmek de zordur. Düşündüğünü taklit etmek her zaman daha kolaydır. Burada koşma ile bir benzetme yapabilirsiniz - ne kadar az koşarsanız, o kadar yavaş koşarsınız. Kaslarınızı eğitmeniz ve yazma pratiği yapmanız gerekiyor. Uygulamaya ihtiyacım var.
Spesifikasyon yanlış olabilir. Bir yerde hata yapmış olabilirsiniz veya gereksinimler değişmiş olabilir veya bir iyileştirme yapılması gerekebilir. Herhangi birinin kullandığı herhangi bir kod değiştirilmelidir, böylece er ya da geç belirtim artık programla eşleşmeyecektir. İdeal olarak, bu durumda, yeni bir özellik yazmanız ve kodu tamamen yeniden yazmanız gerekir. Kimsenin bunu yapmadığını çok iyi biliyoruz. Pratikte, koda yama yaparız ve muhtemelen spesifikasyonu güncelleriz. Eğer bu er ya da geç gerçekleşecekse, o zaman neden spesifikasyonlar yazalım? İlk olarak, kodunuzu düzenleyecek kişi için, şartnamedeki fazladan her kelime ağırlığınca altın değerinde olacaktır ve bu kişi pekala siz olabilirsiniz. Kodumu düzenlerken yeterince spesifikasyon alamadığım için sık sık kendimi azarlarım. Ve koddan çok özellik yazıyorum. Bu nedenle, kodu düzenlediğinizde, spesifikasyonun her zaman güncellenmesi gerekir. İkincisi, her revizyonda kod daha da kötüleşir, okunması ve bakımı giderek daha zor hale gelir. Bu entropide bir artıştır. Ancak bir spesifikasyonla başlamazsanız, yazdığınız her satır bir düzenleme olacaktır ve kod hantal olacak ve baştan okunması zor olacaktır.
Dediği gibi , hiçbir savaş planla kazanılmadı ve hiçbir savaş plansız kazanılmadı. Ve savaşlar hakkında bir iki şey biliyordu. Spesifikasyon yazmanın zaman kaybı olduğu yönünde bir görüş var. Bazen bu doğrudur ve görev o kadar basittir ki üzerinde düşünülecek hiçbir şey yoktur. Ancak her zaman şunu hatırlamalısınız ki, size şartname yazmamanız söylendiğinde, düşünmemeniz de söylenmektedir. Ve her seferinde bunu düşünmelisin. Görevi baştan sona düşünmek, hata yapmayacağınızı garanti etmez. Bildiğimiz gibi kimse sihirli değneği icat etmedi ve programlama zor bir iştir. Ancak problemi derinlemesine düşünmezseniz, hata yapmanız garantidir.
TLA + ve PlusCal hakkında daha fazla bilgiyi özel bir web sitesinde okuyabilir, oraya ana sayfamdan gidebilirsiniz. . Benim için hepsi bu, ilginiz için teşekkür ederim.
Lütfen bunun bir çeviri olduğunu unutmayın. Yorum yazarken, yazarın onları okumayacağını unutmayın. Yazarla gerçekten sohbet etmek istiyorsanız, o zaman 2019-11 Temmuz 12'da St. Petersburg'da yapılacak olan Hydra 2019 konferansında olacak. Biletler satın alınabilir .
Kaynak: habr.com