Program derivation

In computer science, program derivation is the derivation of a program from its specification, by mathematical means.

To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. The program thus obtained is then correct by construction. Program and correctness proof are constructed together.

The approach usually taken in formal verification is to first write a program, and then provide a proof that it conforms to a given specification. The main problems with this are that:

  • the resulting proof is often long and cumbersome;
  • no insight is given as to how the program was developed; it appears "like a rabbit out of a hat";
  • should the program happen to be incorrect in some subtle way, the attempt to verify it is likely to be long and certain to be fruitless.

Program derivation tries to remedy these shortcomings by:

  • keeping proofs shorter, by development of appropriate mathematical notations;
  • making design decisions through formal manipulation of the specification.

Terms that are roughly synonymous with program derivation are: transformational programming, algorithmics, deductive programming.

The Bird-Meertens Formalism is an approach to program derivation.

Approaches to achieving correctness in Distributed computing include research languages such as the P programming language.

See also

References

  • Edsger W. Dijkstra, Wim H. J. Feijen, A Method of Programming, Addison-Wesley, 1988, 188 pages
  • Edward Cohen, Programming in the 1990s, Springer-Verlag, 1990
  • Anne Kaldewaij, Programming: The Derivation of Algorithms, Prentice-Hall, 1990, 216 pages
  • David Gries, The Science of Programming, Springer-Verlag, 1981, 350 pages
  • Carroll Morgan (computer scientist), Programming from Specifications, International Series in Computer Science (2nd ed.), Prentice-Hall, 1998.
  • Eric C.R. Hehner, a Practical Theory of Programming, 2008, 235 pages
  • A.J.M. van Gasteren. On the Shape of Mathematical Arguments. Lecture Notes in Computer Science #445, Springer-Verlag, 1990. Teaches how to write proofs with clarity and precision.
  • Martin Rem. "Small Programming Exercises", appeared in Science of Computer Programming, Vol.3 (1983) through Vol.14 (1990).
  • Roland Backhouse. Program Construction: Calculating Implementations from Specifications. Wiley, 2003. ISBN 978-0-470-84882-1.
  • Derrick G. Kourie, Bruce W. Watson. The Correctness-by-Construction Approach to Programming. Springer-Verlag, 2012. ISBN 978-3-642-27919-5. Provides a step-by-step explanation of how to derive mathematically correct algorithms using small and tractable refinements.

Read other articles:

Patrick DeLacy

Patrick DeLacyLahir(1835-11-25)25 November 1835Carbondale, PennsylvaniaMeninggal27 April 1915(1915-04-27) (umur 79)PennsylvaniaDikebumikanSaint Catherine's Cemetery, Moscow, PennsylvaniaPengabdian Amerika SerikatDinas/cabangUnited States ArmyUnion ArmyPangkatKapten (keluar dari ketenaraan sebagai letnan)Kesatuan 143rd Pennsylvania Volunteer Infantry Regiment - Company APenghargaan Medal of Honor Civil War Campaign Medal Patrick DeLacy (25 November 1835 – 27 April 191...

 

Lampedusa

The south coast of Lampedusa Lampedusa Locasi di Italia Lampedusa (Italia: Isola di Lampedusa) merupakan pulau terbesar di Kepulauan Pelagie dan terletak 205 km dari Sisilia dan 113 km dari Tunisia. Penduduk utamanya terdiri dari perikanan, pertanian, dan pariwisata. Pulau ini terletak di Region Sisilia, provinsi Agrigento, Italia. Penduduknya berjumlah 6.025 jiwa dan luas wilayah 25,48 km². Koordinat: 35°30′N 12°36′E / 35.500°N 12.600°E / 35.50...

 

Gestion durable des forêts

Pays participant au programme UNREDD (en) et/ou au partenariat Forest Carbon Partnership Facility. Déforestation d'une forêt atlantique à Rio de Janeiro afin d'extraire de l'argile destiné à la construction du quartier de Barra da Tijuca (2009). Un exemple d'espace non-géré. La gestion durable des forêts ou l'aménagement écosystémique des forêts est un mode de sylviculture à tendance écologique qui fixe des critères, indicateurs[1] et objectifs sociaux et environnementaux,...

Robert Weakley

American politician (1764–1845) Robert WeakleyPortrait of Weakley by Washington B. CooperMember of the U.S. House of Representativesfrom Tennessee's 2nd districtIn officeMarch 4, 1809 – March 3, 1811Preceded byGeorge W. CampbellSucceeded byJohn SevierMember of the Tennessee SenateIn office1799180318071819 Personal detailsBorn(1764-07-20)July 20, 1764Halifax County, Virginia Colony, British AmericaDiedFebruary 4, 1845(1845-02-04) (aged 80)Nashville, Tennessee, U.S...

 

Targum

Alkitab Ibrani dari abad ke-11 dengan targum, kemungkinan dari Tunisia, ditemukan di Irak: bagian dari Schøyen Collection. Targum (bentuk jamak targumim, Ibrani: תרגםום) adalah penjelasan, parafrasa dan pengembangan lisan mengenai Alkitab Ibrani yang diberikan oleh para rabbi dalam bahasa sehari-hari kepada para pendengarnya, pada periode di mana bahasa yang dipakai adalah bahasa Aram. Hal ini diperlukan karena menjelang akhir abad menjelang munculnya Kekristenan, bahasa umum sedan...

 

Koloni Singapura

Koloni SingapuraColony of Singapore1946–1963 Top: Flag (1946–1959) Bottom: Flag (1959–1963) Lambang negara tahun 1826-1946 (atas), Lambang tahun (1946-1959) (bawah, kini sebagai lambang Singapura) Lagu kebangsaan: God Save the King/Queen (1826-1959)Majulah Singapura (1959-1963)Letak Singapura dalam Kepulauan MelayuStatusKoloni MahkotaIbu kotaSingaporeBahasa yang umum digunakanInggrisMelayuMandarinbahasa-bahasa IndiaPemerintahanMonarkiPenguasa • 1936–1952 George V...

24th National Film Awards

Indian ceremony celebrating cinema of 1976 This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: 24th National Film Awards – news · newspapers · books · scholar · JSTOR (April 2013) (Learn how and when to remove this message) 24th National Film AwardsAwarded forBest of Indian cinema in 1976Awarded byDirectorate of...

 

Neuvy (Marne)

Pour les articles homonymes, voir Neuvy. Cet article est une ébauche concernant une commune de la Marne. Vous pouvez partager vos connaissances en l’améliorant (comment ?). Le bandeau {{ébauche}} peut être enlevé et l’article évalué comme étant au stade « Bon début » quand il comporte assez de renseignements encyclopédiques concernant la commune. Si vous avez un doute, l’atelier de lecture du projet Communes de France est à votre disposition pour vous aider....

 

Paolo Grossi (calciatore)

Paolo Grossi Nazionalità  Italia Altezza 180 cm Peso 78 kg Calcio Ruolo Centrocampista Termine carriera 1º luglio 2021 CarrieraGiovanili 2002-2004 MilanSquadre di club1 2004-2006 Caratese59 (12)2006-2009 Varese92 (18)2009-2011→  AlbinoLeffe39 (9)[1]2011-2012 Siena11 (1)2012-2013 Verona16 (0)2013→  Pro Vercelli6 (1)2013-2014→  Brescia32 (4)2014-2015→  Virtus Lanciano30 (3)2015-2016 Ternana22 (0)2016-2017 Arezzo21 (4...

Правильный пятиугольник

Иное название этого понятия — «Пентагон»; см. также другие значения. Пятиугольник Правильный пятиугольник Тип Правильный многоугольник Рёбра 5 Символ Шлефли {5} Диаграмма Коксетера — Дынкина Вид симметрии Диэдрическая группа (D5) Площадь t 2 25 + 10 5 4 = {\displaystyle {\frac {t^{2}{\sqrt {25...

 

71e cérémonie des British Academy Film Awards

71e cérémonie des British Academy Film Awards British Academy Film Awards Organisée par la British Academy of Film and Television Arts Détails Date 18 février 2018 Lieu Royal Albert Hall, Londres Royaume-Uni Présentateur Joanna Lumley Site web http://www.bafta.org/ Résumé Meilleur film Three Billboards : Les Panneaux de la vengeance Meilleur film britannique Three Billboards : Les Panneaux de la vengeance Film le plus nommé La Forme de l'eau (12) Film le plus récompe...

 

Северный морской котик

Северный морской котик Самец Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:Синапси...

Franklin Chang-Díaz

Costa Rican-American astronaut and entrepreneur (born 1950) In this Spanish name, the first or paternal surname is Chang and the second or maternal family name is Díaz. Franklin Chang-DíazChang-Díaz in 1997BornFranklin Ramón Chang-Díaz (1950-04-05) April 5, 1950 (age 74)San José, Costa RicaEducationUniversity of Connecticut (BS)Massachusetts Institute of Technology (MS, ScD)ChildrenSoniaSpace careerNASA astronautTime in space66d 18h 16mSelectionNASA Group 9 (1980)MissionsST...

 

Cherry Jones

Cherry JonesJones at 24's season 7 finale screening in 2009Lahir21 November 1956 (umur 67)Paris, Tennessee, U.S.AlmamaterCarnegie Mellon UniversityPekerjaanActressTahun aktif1980–presentSuami/istriSophie Huber ​(m. 2015)​PasanganSarah Paulson (2004–2009) Cherry Jones (lahir 21 November 1956) adalah aktris berkebangsaan Amerika Serikat. Namanya dikenal secara luas ketika dia dinominasikan sebanyak lima kali menerima penghargaan Tony Award untuk p...

 

Category (mathematics)

Mathematical object that generalizes the standard notions of sets and functions For other uses, see Category (disambiguation) § Mathematics. This is a category with a collection of objects A, B, C and collection of morphisms denoted f, g, g ∘ f, and the loops are the identity arrows. This category is typically denoted by a boldface 3. In mathematics, a category (sometimes called an abstract category to distinguish it from a concrete category) is a collection of objects that are linked...

ダーティハリー

ダーティハリー Dirty Harry 監督 ドン・シーゲル脚本 ハリー・ジュリアン・フィンク（英語版）R・M・フィンク（英語版）ディーン・リーズナー（英語版）原案 ハリー・ジュリアン・フィンクR・M・フィンク製作 ドン・シーゲル製作総指揮 ロバート・デイリー出演者 クリント・イーストウッドアンディ・ロビンソンハリー・ガーディノレニ・サントーニジョン・ミッチ�...

 

低層建築物

低層建築物（ていそうけんちくぶつ）は、高さによって建築物を区分する際の一区分で、一般に1階（平屋）及び2階建ての建築物を指すが、3階建てを含めることもある[1]。低層建築物より高さが高い建築物は、順に中層建築物、高層建築物と呼ばれる。 定義 建設省が1995年に策定した「長寿社会対応住宅設計指針」（建設省住備発第63号）[2]においては、「6�...

 

Stångstörtning

Traditional Swedish sport A 2006 stångstörtning competition Stångstörtning is a Swedish sport originating from Gotland. It is similar to the Scottish caber toss, and involves tossing a log as far as possible. The log is 4.2–4.5 m long, weighs 26–27 kg, has a diameter of 13 cm at the thick end and 6–7 cm at the thin end, and is made of Norway spruce.[1] It is contested at the Stånga Games,[2] and was an unofficial demonstration event at the 1912 Summer Olympics along...

Kingdom of Kinda

Ancient Arabian polity Kingdom of Kindaكِنْدَة الملوكc. 450 CE–c. 550 CEMap showing approximate extent of the Kingdom of Kinda, c. 500 CECapitalGhamr Dhi KindaBatn AqilQaryat al-FawHajaral-MushaqqarCommon languagesArabicReligion Christianity, Arabian polytheismDemonym(s)KinditesGovernmentMonarchyHistory • Established c. 450 CE• Disestablished c. 550 CE Today part ofSaudi Arabia The Kingdom of Kinda (Arabic: كِنْدَة ا...

 

Messinian salinity crisis

Drying-up of the Mediterranean Sea from 5.96 to 5.33 million years ago Artistic interpretation of the Mediterranean geography during its evaporative drawdown, after complete disconnection from the Atlantic. The rivers carved deep gorges in the exposed continental margins; The concentration of salt in the remaining water bodies led to rapid precipitation of the salt. The inset evokes the transit of mammals (e.g. camels and mice) from Africa to Iberia across the exposed Gibraltar Strait. In the...