Szerkesztő:Kovacsshotput/próbalap

A Hoare-logika

A Hoare-logika(más néven Floyd-Hoare-logika vagy a Hoare-szabályok) ez egy olyan formális rendszerrel amely logikai szabályok halmazát tartalmazza a számítógépes programok helyességének szigorú bizonyítására.Tony Hoare,brit számítógéptudós és logikus dolgozta ki 1969-ben, majd később finomították Hoare és más kutatók. ^[1] Az eredeti ötletek Robert W. Floyd,munkájának hatására születtek, aki hasonló rendszert publikált^[2] folyamatábrákhoz.

Hoare hármas

A Hoare-logika központi eleme a Hoare hármas. Ez a hármas leírja, hogy a kódrészlet végrehajtása hogyan változtatja meg a számítás állapotát. A Hoare hármas formailag

\{P\}C\{Q\}

ahol $P$ és $Q$ állítások és $C$ pedig egy parancs.^{[note 1]} $P$ -t nevezzük előfeltételnek és $Q$ -t pedig utófeltételnek: amikor az előfeltétel teljesül, a parancs végrehajtása teljesíti az utófeltételt. Az állítások predikátumlogikai formulák.

A Hoare-logika biztosít axiómákat és következtetési szabályokat egy egyszerű imperative programozási nyelv valamennyi konstrukciójához. Az eredeti Hoare-kutatásokban szereplő egyszerű nyelv szabályai mellett azóta számos más nyelvi konstrukcióhoz készítettek szabályokat Hoare és más kutatók. Vannak szabályok concurrency, eljárásokhoz, ugrásokhoz, és mutatókhoz.

Részleges és teljes helyesség

Az alapvető Hoare-logikával csak a részleges helyesség bizonyítható. A teljes helyesség külön bizonyítást igényel a határokra vonatkozóan, amelyet kiterjesztett verziójú While-szabállyal vagy külön bizonyítással lehet megadni.^[3] Így egy Hoare-hármas intuitív értelmezése a következő: Ha $P$ igaz a számítás állapotára a $C$ , végrehajtása előtt, akkor a $Q$ igaz lesz , vagy, $C$ nem terminálódik. Utóbbi esetben nincs "után", ezért a $Q$ bármely megállapítás lehet. Valójában a $Q$ választható hamis értékűnek annak kifejezésére, hogy $C$ nem határolódik.

A "terminálás" itt és a cikk további részében a számítás végső befejezését jelenti a széles értelmezésben, ami azt jelenti, hogy az eljárás végső soron befejeződik, és az örökké tartó ciklusok hiányát jelenti; nem jelenti a megvalósítási korlátok megsértése (pl. nullával való osztás) hiányát, ami korai programleálláshoz vezethet. Hoare 1969-es cikkében szűkebb terminálási fogalmat használt, amely a megvalósítási korlátok hiányát is magában foglalta, és széles értelmezésű terminálás mellett érvelt, mivel az megőrzi az állítások megvalósításfüggetlenségét:^[4]

„A másik hiányosság az idézett axiómákban és szabályokban az, hogy nem nyújtanak alapot egy program sikeres leállásának bizonyításához. A leállás meghiúsulhat egy végtelen ciklus miatt, vagy az implementáció által meghatározott határértékek megsértése miatt, például a numerikus operandusok tartománya, a tároló mérete vagy egy operációs rendszer időkorláta miatt. Ezért a “

P{Q}R

” jelölést úgy kell értelmezni, hogy “amennyiben a program sikeresen leáll, az eredményeinek tulajdonságai a

R

által leírtak szerinti.” Viszonylag könnyű azzal módosítani az axiómákat, hogy ne lehessen velük megjósolni a nem leálló programok “eredményeit”, azonban az axiómák használata mostantól függene az implementáció sok függő tulajdonságától, például a számítógép sebességétől és méretétől, a számok tartományától és az overflow technika választásától. A végtelen ciklusok elkerülésének bizonyításán kívül valószínűleg jobb a program “feltételes” helyességét bizonyítani, és a végrehajtás megszakításakor az implementáció figyelmeztetésére támaszkodni, ha a program végrehajtását az implementációs korlát megsértése miatt fel kellett függeszteni.A másik hiányosság az idézett axiómákban és szabályokban az, hogy nem nyújtanak alapot egy program sikeres leállásának bizonyításához. Az leállás meghiúsulhat egy végtelen ciklus miatt, vagy az implementáció által meghatározott határértékek megsértése miatt, például a numerikus operandusok tartománya, a tároló mérete vagy egy operációs rendszer időkorláta miatt. Ezért a “

P{Q}R

” jelölést úgy kell értelmezni, hogy “amennyiben a program sikeresen leáll, az eredményeinek tulajdonságai a

R

által leírtak szerinti.” Viszonylag könnyű azzal módosítani az axiómákat, hogy ne lehessen velük megjósolni a nem leálló programok “eredményeit”, azonban az axiómák használata mostantól függene az implementáció sok függő tulajdonságától, például a számítógép sebességétől és méretétől, a számok tartományától és az overflow technika választásától. A végtelen ciklusok elkerülésének bizonyításán kívül valószínűleg jobb a program “feltételes” helyességét bizonyítani, és a végrehajtás megszakításakor az implementáció figyelmeztetésére támaszkodni, ha a program végrehajtását az implementációs korlát megsértése miatt fel kellett függeszteni. ”

Szabályok

Üres feltétel alaptétel

Az üres feltétel nem változtatja meg a program állapotát, így bármi, ami igaz volt az üres utasítás előtt, az utasítás után is igaz marad.^{[note 2]}

{\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}

Az értékadás alaptétel

Az értékadás axióma azt állítja, hogy az értékadás után bármely olyan állítás, amely korábban igaz volt az értékadás jobb oldalára vonatkozóan, most igaz a változóra is. Formálisan legyen P egy olyan állítás, amelyben az x változó szabadon szerepel. Ekkor:

{\dfrac {}{\{P[E/x]\}x:=E\{P\}}}

ahol $P[E/x]$ utal a P állításra ,azt jelent, ahol hogy az összes x szabad előfordulását $x$ kicserélődik $E$ -re.

z értékadás axióma sémája azt jelenti, hogy az $P[E/x]$ igazsága ekvivalens a P utáni állítással. Ha tehát $P[E/x]$ igaz volt az értékadás előtt, akkor az értékadás axiómája alapján $P$ igaz lesz a későbbiekben is. Ha viszont $P[E/x]$ hamis (azaz. $\neg P[E/x]$ igaz) akkor az értékadás után, $P$ hamisnak kell lennie.

Példák érvényes hármasra:

$\{x+1=43\}y:=x+1\{y=43\}$
$\{x+1\leq N\}x:=x+1\{x\leq N\}$

Azokat a feltételeket, amelyeket az kifejezés nem módosít, át lehet vinni a post-állapotba.Az első példában a $y:=x+1$ értékadás nem változtatja meg azt a tényt, hogy $x+1=43$ , így mindkét állítás szerepelhet a post-állapotban. Formálisan ezt az eredményt az axióma sémájának alkalmazásával érhetjük el, ahol $P$ ( $y=43$ és $x+1=43$ ), ahol átad $P[(x+1)/y]$ ahol ( $x+1=43$ and $x+1=43$ ),amelyet a kiinduló feltételre $x+1=43$ egyszerűsíthető le.

Egy másik helytelen szabály, amely első pillantásra csábítónak tűnik: {P}x:=E{P∧x=E} ; értelmetlen példákhoz vezet, például:

{x=5}x:=x+1{x=5∧x=x+1}

Bár egy adott postcondition P egyértelműen meghatározza a precondition-t P[E/x], a fordított irányítás nem igaz. Például:

Az értékadás tétel séma ekvivalens azzal az állítással, hogy az előfeltétel meghatározásához először vegyük az utófeltételt-t, és cseréljük ki az összes bal oldali kifejezést az értékadás jobb oldali kifejezésével. Vigyázzunk, hogy ne próbáljuk ezt visszafelé megtenni az alábbi helytelen gondolatmenet követése során: $\{P\}x:=E\{P[E/x]\}$ ; ez a szabály értelmetlen példákhoz vezet, ehez hasonlókhoz:

\{x=5\}x:=3\{3=5\}

Egy másik helytelen szabály, amely első pillantásra csábítónak tűnik: $\{P\}x:=E\{P\wedge x=E\}$ ; értelmetlen példákhoz vezet, például:

\{x=5\}x:=x+1\{x=5\wedge x=x+1\}

Bár egy adott utófeltétel $P$ egyértelműen meghatározza az előfeltételt $P[E/x]$ , megfordítva ez nem igaz.

Példa:

$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}$ , and
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}$

are valid instances of the assignment axiom scheme.

Az elosztás alaptétele Hoare által javasolt szabálya nem alkalmazható, ha több név is hivatkozhat ugyanarra az értékre.

Példa,

\{y=3\}x:=2\{y=3\}

ha az x és y változók ugyanarra az értékre hivatkoznak (aliasing), akkor az alábbi kódrészlet nem helyes,ugyanakkor ez egy helyes példa (mind a

\{P\}

és

\{P[2/x]\}

ugyanúgy

\{y=3\}

).

Elrendezési szabálya

A csere kódjának ellenőrzése

segédváltozók nélkül.

Az alábbi három állítás (2., 4. és 6. sor) kicseréli az a és b változók értékeit, segédváltozó nélkül. A verifikációs bizonyítékban a kezdeti értékek A és B konstansokkal vannak jelölve. A bizonyítást érdemes visszafelé olvasni, a 7. sorból kiindulva; például az 5. sort a 7-es kifejezésben szereplő a helyettesítésével kapjuk meg, amelyet az a−b (6. sorban szereplő forrás kifejezés) helyettesít. Néhány számtani egyszerűsítést hallgatólagosan használnak, például a−(a−b)=b (5. sor→3. sor), és, a+b−b=a (3. sor→1. sor).
Szám	Kód	Állítás
1:		$\{a=A\wedge b=B\}$
2:	$a:=a+b;$
3:		$\{a-b=A\wedge b=B\}$
4:	$b:=a-b;$
5:		$\{b=A\wedge a-b=B\}$
6:	$a:=a-b$
7:		$\{b=A\wedge a=B\}$

Hoare elrendezési szabálya sorban folyamatosan hajtja végre a programot, S-re és T-re ahol S végrehajtása előbb történik majd utána a T-é, és az így írható: $S;T$ ( $Q$ a köztes állapotot jelöli):^[5]

{\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}

Például,vegyük figyelembe a következő két esetet értékadás tételével

\{x+1=43\}y:=x+1\{y=43\}

és

\{y=43\}z:=y\{z=43\}

Az elrendezés szabály alkalmazásával azt állapíthatjuk meg:

\{x+1=43\}y:=x+1;z:=y\{z=43\}

Egy másik példa a jobb oldali táblázatban van.

Feltételes szabály

{\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}

A feltételes szabály szerint, egy $Q$ utóállapot, amely közös then és else részre, az egész if...endif utasítás utóállapota is..^[6] A then és a else részben,a dupla tagadás és a tagadott feltétel $B$ hozzáadható a feltétel $P$ előfeltételéhez, és ez kölcsönös. $B$ feltételének, nincsen mellékhatása.Egy példa a következő részben látható.

Ez a szabály nem volt benne Hoare eredeti publikációjában.^[1] Azonban, mivel az állítás:

{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}

ugyanazt az eredményt adja, mint egy egyszeri ciklus konstrukció

{\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {done}}

a feltételes szabály származtatható a többi Hoare-szabályból. Hasonlóan, más szabályokhoz , a származtatott program szerkezetekre, mint a for loop, do...until loop, switch, break, continue lehet átalakítani a Hoare eredeti írásaból származó szabályokra.

Következmény szabály

{\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}

Ez a szabály lehetővé teszi, hogy megerősítsük az előfeltételt $P_{2}$ és/vagy gyengítsük a végfeltételt $Q_{2}$ . Ezt például akkor használjuk, ha a "then" és " else" ágak végfeltételek.

Például a következő bizonyítás:

\{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}

A feltételes szabály alkalmazásához először bizonyítani kell, hogy:

\{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}

, vagy egyszerűsítve:

\{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}

a then részhez, és

\{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}

, vagy egyszerűsítve:

\{x=15\}x:=0\{0\leq x\leq 15\}

a else részhez.

Ugyanakkor,értékadás szabálya a then résszel az várja el hogy $P$ az $0\leq x\leq 15$ ; szabály alkalmazásával ezentúl megengedett

\{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}

, ami logikusan ekvivalens

\{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}

.

A következményszabály az előfeltétel megerősítéséhez szükséges $\{-1\leq x<15\}$ a hozzárendelési szabályból kapott $\{0\leq x<15\}$ feltételes szabályhoz szükséges.

Hasonlóan, az else résszel, az értékadás szabály megengedi

\{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}

, vagy megegyezően

\{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}

,

ezért a következményszabályt kell alkalmazni $P_{1}$ és $P_{2}$ lény $\{x=15\}$ és $\{{\texttt {true}}\}$ , illetve, hogy ismét erősítse az előfeltételt. Informálisan a következményszabály hatása az, hogy ezt "elfelejti". $\{x=15\}$

$\{x=15\}$ bejegyzésénél ismertelse részét, mivel a hozzárendelési szabályt használják az else résznek nincs szüksége erre az információra..

Míg szabály

{\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}\{\neg B\wedge P\}}}

Itt $P$ a hurokinvariáns, amelyet az $S$ huroktestnek meg kell őriznie. A ciklus befejezése után ez az invariáns $P$ továbbra is érvényes, sőt $\neg B$ biztosan véget ért a hurok. A feltételes szabályhoz hasonlóan $B$ nem lehetnek mellékhatásai.

Például, bizonyításként

\{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}

a Míg szabály bizonyítja hogy

\{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}

, vagy egyszerűsíte

\{x<10\}x:=x+1\{x\leq 10\}

,

Ezt könnyedén megkaphatjuk az "értékadás szabályával". Végül a utófeltétel, $\{\neg x<10\wedge x\leq 10\}$ lelehet egyszerűsíteni $\{x=10\}$ .

Egy következő példa, "mindaddig" szabály formális igazolására az alábbi furcsa program, amely egy tetszőleges szám a pontos gyökének $x$ kiszámítására szolgál - még akkor is, ha $x$ egy egész szám változó és a nem négyzetszám:

\{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}

miután alkalmaztuk a mindaddig szabályt $P$ true, az marad, hogy bebizonyítsuk

\{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}

,

Ez abból következik, hogy alkalmazzuk az "üres utasítás" szabályt és a következmény szabályt

Valójában a furcsa program részben helyes: ha véletlenül véget ér, akkor biztos, hogy $x$ értéke tartalmazza a ' $a$ ' négyzetgyökét. Minden más esetben nem fog véget érni, így nem teljesen mértében helyes.

Mindaddig szabály a teljes helyesség érdekében

Ha a fenti egyszerű mindaddig szabályt a következővel helyettesítjük, akkor a Hoare-féle kalkulus alkalmas lehet a teljes helyesség, azaz a terminálás és a részleges helyesség bizonyítására is. Általában szögletes zárójeleket használnak itt a program helyességének különböző fogalmának jelzésére.

{\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}

Ebben a szabályban az ismétlési invariáns mellett a leállási feltételt is bizonyítani kell egy kifejezés $t$ segítségével, amelynek értéke szigorúan csökken egy jól-alapuló reláció szerint egy adott < t $D$ tartományban minden iteráció során. Mivel a < reláció jól-alapuló, a D tagjainak szigorúan csökkenő láncolata csak véges hosszúságú lehet, így a t értéke nem csökkenhet örökké. (Például a szokásos < sorrend jól-alapuló a pozitív egész számok $\mathbb {N}$ halmazán, de nem jól-alapuló sem az egész számok $\mathbb {Z}$ halmazán, sem a pozitív valós számok $\mathbb {R} ^{+}$ halmazán; ezek az összes halmaz matematikai értelemben vett végtelen halmazok.)

Az ismétlési invariáns $P$ megadása mellett a feltételnek $B$ biztosítania kell, hogy $t$ nem minimális eleme $D$ -nek, különben a test $S$ nem tudná tovább csökkenteni a $t$ értékét, vagyis a szabály feltétele nem lenne teljesülve. (Ez az egyik jelölése a teljes helyességnek.) ^{[note 3]}

A korábbi rész első példájának folytatásaként, a következő teljes helyességgel kapcsolatos bizonyításhoz:

[x\leq 10]{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}[\neg x<10\wedge x\leq 10]

a teljes helyességű mindaddig szabályt alkalmazhatjuk, például a $D$ halmaz az egész számok, a hagyományos relációval < , az $t$ kifejezése pedig $10-x$ , amely akkor bebizonyítja

[x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]

Nem annyira hivatalosan szólva, azt kell bizonyítanunk, hogy a távolság $10-x$ minden ciklusban csökken, miközben mindig nem-negatív marad; ez a folyamat csak véges számú cikluson keresztül tarthat.

Az előző bizonyítási cél egyszerűsíthető a következőre:

[x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]

,

Ezt a következőképpen lehet bizonyítani:

[x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]

a hozzárendelési szabály segítségével áll elő, és

[x+1\leq 10\wedge 10-x-1<z]

can be strengthened to

[x<10\wedge 10-x=z]

következmény szabály segítségével erősíthető fel

A második példájában ebben a részben nyilvánvalóan nem található olyan kifejezés $t$ , amelyet az üres ciklustörzs csökkentene, így a termináció nem bizonyítható.

Továbbiak

* Assertion (software development)

Megjegyzések

↑ Hoare originally wrote " $P\{C\}Q$ " rather than " $\{P\}C\{Q\}$ ".
↑ This article uses a natural deduction style notation for rules. For example, ${\dfrac {\alpha ,\beta }{\phi }}$ informally means "If both $α$ and $β$ hold, then also $φ$ holds"; $α$ and $β$ are called antecedents of the rule, $φ$ is called its succedent. A rule without antecedents is called an axiom, and written as ${\dfrac {}{\quad \phi \quad }}$ .
↑ Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook^[3] gives the following version of a total correctness rule: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ when $z$ is an integer variable that doesn't occur free in $P$ , $B$ , $S$ , or $t$ , and $t$ is an integer expression (Reynolds' variables renamed to fit with this article's settings).

Jegyzetek

↑ ^a ^b (1969. október 1.) „An axiomatic basis for computer programming”. Communications of the ACM 12 (10), 576–580. o. DOI:10.1145/363235.363259.
↑ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.
↑ ^a ^b John C. Reynolds. Theory of Programming Languages. Cambridge University Press (2009) ) Here: Sect. 3.4, p. 64.
↑ Hoare (1969), p.578-579
↑ Logic in Computer Science, second, CUP, 276. o. (2004. augusztus 26.). ISBN 978-0521543101
↑ (2019. december 1.) „Fifty years of Hoare's logic”. Formal Aspects of Computing 31 (6), 759. o. DOI:10.1007/s00165-019-00501-3.

További olvasmányok

Robert D. Tennent. Specifying Software (a tankönyv mely tartalmazza Hoare-logikát 2002-ben jelent meg. ) ISBN 0-521-00401-2

Külső linkek

KeY-Hoare A KeY-re támaszkodó részben automatikus verifikációs rendszer. Egyszerű while nyelvhez tartalmaz Hoare-féle számításokat.
j-Algo-modul Hoare calculus — A Hoare-kalkulus vizualizációja a j-Algo algoritmus-ábrázoló programban.

Sablon:Program analysis

[3] Hoare originally wrote " $P\{C\}Q$ " rather than " $\{P\}C\{Q\}$ ".

[6] This article uses a natural deduction style notation for rules. For example, ${\dfrac {\alpha ,\beta }{\phi }}$ informally means "If both $α$ and $β$ hold, then also $φ$ holds"; $α$ and $β$ are called antecedents of the rule, $φ$ is called its succedent. A rule without antecedents is called an axiom, and written as ${\dfrac {}{\quad \phi \quad }}$ .

[9] Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook^[3] gives the following version of a total correctness rule: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ when $z$ is an integer variable that doesn't occur free in $P$ , $B$ , $S$ , or $t$ , and $t$ is an integer expression (Reynolds' variables renamed to fit with this article's settings).

[hoare-1] (1969. október 1.) „An axiomatic basis for computer programming”. Communications of the ACM 12 (10), 576–580. o. DOI:10.1145/363235.363259.

[2] R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.

[Reynolds.2009-4] John C. Reynolds. Theory of Programming Languages. Cambridge University Press (2009) ) Here: Sect. 3.4, p. 64.

[5] Hoare (1969), p.578-579

[7] Logic in Computer Science, second, CUP, 276. o. (2004. augusztus 26.). ISBN 978-0521543101

[8] (2019. december 1.) „Fifty years of Hoare's logic”. Formal Aspects of Computing 31 (6), 759. o. DOI:10.1007/s00165-019-00501-3.

[1]

[2]

[note 1]

[3]

[4]

[note 2]

[5]

[6]

[note 3]