Enande teorier om programmering

Unifying Theories of Programming ( UTP ) inom datavetenskap handlar om programsemantik . Den visar hur denotationssemantik , operationell semantik och algebraisk semantik kan kombineras i ett enhetligt ramverk för formell specifikation , design och implementering av program och datorsystem .

Boken med denna titel av CAR Hoare och He Jifeng publicerades i Prentice Hall International Series in Computer Science 1998 och är nu fritt tillgänglig på webben.

Teorier

Den semantiska grunden för UTP är den första ordningens predikatkalkyl, utökad med fixpunktskonstruktioner från andra ordningens logik. Enligt Eric Hehners tradition är program predikat i UTP, och det finns ingen skillnad mellan program och specifikationer på semantisk nivå . Med Hoares ord :

Ett datorprogram identifieras med det starkaste predikatet som beskriver varje relevant observation som kan göras av beteendet hos en dator som exekverar programmet.

I UTP-språk är en teori en modell av ett visst programmeringsparadigm. En UTP-teori består av tre ingredienser:

ett alfabet , som är en uppsättning variabelnamn som anger paradigmets attribut som kan observeras av en extern enhet;
en signatur , som är uppsättningen av programmeringsspråkskonstruktioner som är inneboende i paradigmet; och
en samling hälsoförhållanden , som definierar utrymmet för program som passar inom paradigmet. Dessa hälsotillstånd uttrycks vanligtvis som monotona idempotenta predikattransformatorer .

Programförfining är ett viktigt begrepp i UTP. Ett program $P_{1}$ förfinas med $P_{2}$ om och endast om varje observation som kan göras av $P_{2}$ också är en observation av $P_{1}$ . Definitionen av förfining är vanlig i UTP-teorier:

$P_{1}\sqsubseteq P_{2}\quad {\text{if and only if}}\quad \left[P_{2} \Rightarrow P_{1}\right]$

där $\left[X\right]$ anger den universella stängningen av alla variabler i alfabetet.

Relationer

Den mest grundläggande UTP-teorin är den alfabetiserade predikatkalkylen, som inte har några alfabetsbegränsningar eller hälsovillkor. Relationsteorin är något mer specialiserad, eftersom en relations alfabet kan bestå av endast:

odekorerade variabler ( $v$ ), modellerar en observation av programmet i början av dess exekvering; och
primerade variabler ( $v'$ ), modellerar en observation av programmet i ett senare skede av dess exekvering.

Vissa vanliga språkkonstruktioner kan definieras i relationsteorin enligt följande:

Skip-satsen, som inte ändrar programtillståndet på något sätt, är modellerad som den relationella identiteten:

$\mathbf {hoppa över} \equiv v'=v$

Tilldelningen av värdet $E$ till en variabel $a$ modelleras som att sätta $a'$ till $E$ och behålla alla andra variabler (betecknade med $u$ ) konstant: