Hoareova logika

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 15. června 2021; kontroly vyžadují 2 úpravy .

Hoareova logika ( angl. Hoare logic , též Floyd-Hoare logic , nebo Hoare rules ) je formální systém se sadou logických pravidel určených k prokázání správnosti počítačové programy . To bylo navrženo v roce 1969 anglickým počítačovým vědcem a matematickým logikem Hoareem , později vyvinutým samotným Hoareem a dalšími výzkumníky. [1] Původní nápad navrhl Floyd , který publikoval podobný systém [2 ] aplikovaný na vývojové diagramy .

Hoare triplets

Hlavní charakteristikou Hoareovy logiky je Hoareova trojice . Trojka popisuje, jak provedení části kódu změní stav výpočtu. Hoareův trojitý má následující podobu:

\{P\}\;C\;\{Q\}

kde P a Q jsou tvrzení a C je příkaz . _ _ _ P se nazývá předběžná podmínka ( antecedent ) a Q se nazývá postpodmínka ( následná ). Pokud je předběžná podmínka pravdivá, příkaz učiní postpodmínku pravdivou. Příkazy jsou formule predikátové logiky .

Hoareova logika má axiomy a pravidla odvození pro všechny konstrukce jednoduchého imperativního programovacího jazyka . Kromě těchto konstrukcí popsaných v původní práci Hoareho vyvinul Hoare a další pravidla pro další konstrukce: souběžné provádění , volání procedury , skok a ukazatel .

Hoareho hlavní myšlenkou je dát každé konstrukci imperativního jazyka pre- a post- podmínku , zapsanou jako logický vzorec. V názvu se proto objevuje trojka - precondition , konstrukce jazyka, postcondition .

Je jasné, že pro prázdný operátor se pre- a postpodmínky shodují.
U operátoru přiřazení v postcondition musí být kromě preconditionu brán v úvahu i fakt, že se změnila hodnota proměnné.
Pro složený příkaz (v Pythonu je to odsazení, v C je to {} ) máme řetězec před- a post- podmínek . Výsledkem je, že první předběžná podmínka a poslední přídavná podmínka mohou být ponechány pro složený příkaz .
Inferenční pravidlo říká, že můžeme posílit předpoklad a oslabit postpodmínku , pokud to potřebujeme. Nemá smysl udržovat v celém programu nějaký druh prohlášení, které nepomůže problém vyřešit.
Výpis pobočky nebo jen kdyby . Může být podmíněně rozdělena do dvou větví: potom a jinak . Pokud k předběžné podmínce (co je pod if ) přidáme pravdivost logické podmínky , pak po provedení větve then by měla následovat postpodmínka . Podobně, pokud k předběžné podmínce (co je pod if ) přidáme negaci logické podmínky , pak by po provedení větve else měla následovat postpodmínka
operátor smyčky. Toto je nejnetriviálnější a nejsložitější, protože smyčka může být provedena mnohokrát a dokonce ani nekončí. Pro vyřešení problému možného opakovaného opakování těla smyčky je zaveden invariant smyčky . Invariantní smyčka je něco, co je pravdivé před provedením, je pravdivé po každém provedení těla smyčky, a je tedy pravdivé i po skončení smyčky. Předpokladem pro příkaz smyčky je jednoduše její invariant smyčky . Pokud je podmínka pokračování smyčky pravdivá (co je pod while ), pak by po provedení těla smyčky měla následovat pravda invariantu smyčky . Výsledkem je, že po skončení cyklu máme jako postpodmínku pravdivost invariantu cyklu a negaci podmínky pokračování cyklu.
Operátor smyčky s plnou správností. K tomu je do předchozího odstavce přidána omezující funkce, pomocí které lze snadno dokázat, že se smyčka bude provádět omezený počet opakování. Jsou na něj kladeny podmínky, že je vždy >=0, přísně klesá po každém provedení těla smyčky a přesně = 0, když smyčka končí.

Dobře fungující program lze napsat mnoha způsoby a v mnoha případech bude efektivní. Tato nejednoznačnost komplikuje programování. Chcete-li to provést, zaveďte styl. Ale to nestačí. U mnoha programů (například těch, které jsou spjaty nepřímo s lidským životem) je navíc nutné prokázat jejich správnost. Ukázalo se, že důkaz správnosti program řádově (asi 10x) prodražuje.

Částečná a úplná správnost

V Hoareho standardní logice lze prokázat pouze částečnou správnost, protože ukončení programu musí být prokázáno samostatně. Také pravidlo nepoužívat nadbytečné části programu nelze vyjádřit v Hoareově logice. "Intuitivní" chápání Hoareovy trojice lze vyjádřit následovně: pokud P nastane před dokončením C , pak buď nastane Q , nebo C nikdy neskončí. Pokud C neskončí, není žádné po, takže Q může být jakýkoli příkaz. Navíc můžeme zvolit Q jako nepravdivé, abychom ukázali, že C nikdy neskončí.

Úplnou správnost lze také prokázat pomocí rozšířené verze pravidla pro příkaz While .

Pravidla

Prázdný operátorový axiom

Pravidlo pro prázdný příkaz říká, že příkaz přeskočit ( prázdný příkaz ) nemění stav programu, takže příkaz, který byl pravdivý před přeskočením , zůstává pravdivý i po jeho provedení.

{\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\))))

Axiom operátoru přiřazení

Axiom operátoru přiřazení říká, že po přiřazení se hodnota libovolného predikátu vzhledem k pravé straně přiřazení nemění s nahrazením pravé strany levou stranou:

{\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\))))

Zde se rozumí výraz P , ve kterém jsou všechny výskyty volné proměnné x nahrazeny výrazem E . $P[E/x]$

Význam axiomu přiřazení je ten, že pravda je po provedení přiřazení ekvivalentní . Pokud to tedy platilo před zadáním, podle axiomu přiřazení to bude platit i po zadání. Naopak, pokud se před příkazem přiřazení rovnalo hodnotě „nepravda“, mělo by se rovnat hodnotě „nepravda“ i poté. $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$

Příklady platných trojic:

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

Axiom přiřazení v Hoareově formulaci neplatí, pokud více než jeden identifikátor odkazuje na stejnou hodnotu. Například,

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

je nepravdivé, pokud x a y odkazují na stejnou proměnnou, protože žádná podmínka nemůže zajistit, aby y bylo 3 poté , co bylo x přiřazeno 2.

Pravidlo kompozice

Hoareovo kompoziční pravidlo platí pro sekvenční provádění programů S a T , kde S se provádí před T , což je zapsáno jako S;T .

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{ R\}}}

Zvažte například dva případy axiomu přiřazení:

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

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

Podle pravidla složení získáme:

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

Pravidlo podmíněného operátoru

{\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\ }\ {\textbf {if}}\ B\ {\textbf {pak}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}

Odvozovací pravidlo

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime )){\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}

Pravidlo příkazu smyčky

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S \ {\textbf {hotovo}}\ \{\neg B\wedge P\}}}

Zde P je invariant cyklu .

Pravidlo příkazu cyklu s plnou správností

{\frac {<\;{\text{je dobře podložený,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P] \ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {hotovo}}\ [\neg B\wedge P]}}

V tomto pravidle se kromě zachování invariantu smyčky dokazuje ukončení smyčky termínem nazývaným proměnná smyčky (zde t ), jejíž hodnota je přísně redukována podle opodstatněného vztahu " < " s každou iterací. V tomto případě musí podmínka B implikovat, že t není minimální prvek její domény, jinak bude premisa tohoto pravidla nepravdivá. Protože vztah " < " je plně podložený, každý krok smyčky je definován klesajícími členy konečné lineárně uspořádané množiny .

Zápis tohoto pravidla používá k označení úplné správnosti pravidla hranaté závorky, nikoli složené závorky. (Toto je jeden ze způsobů, jak označit úplnou správnost.)

Příklady

Příklad 1

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

— na základě axiomu přiřazení.

Protože na základě pravidla odvození dostaneme:

( x + 1 = 43 \Šipka doleva doprava x = 42 )

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

Příklad 2

{\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\))

— na základě axiomu přiřazení.

Pokud jsou x a N celá čísla, pak a na základě pravidla pro odvození dostaneme:

(x < N) \implies (x+1 \leq N)

{\displaystyle \{x<N\}\ x:=x+1\ \{x\leq N\))

Viz také

Odkazy

↑ CAR Hoare . „ Axiomatický základ pro počítačové programování Archivováno 17. července 2011 na Wayback Machine “. Communications of the ACM , 12(10):576-580,583 října 1969. doi : 10.1145/363235.363259
↑ RW Floyd . « Přiřazování slov k programům. Archivováno z originálu 9. prosince 2008. (odkaz dolů od 13-05-2013 [3444 dní] - historie ) » (odkaz ke stažení) Sborník sympozií Americké matematické společnosti o aplikované matematice. sv. 19, str. 19-31. 1967.

Literatura

Guts AK Matematická logika a teorie algoritmů. - M . : Knižní dům "LIBROKOM", 2009. - 117 s. — ISBN 9785397000567 .
https://web.archive.org/web/20110123200456/http://djvu-student.narod.ru/02-matematicheskaya-logika/metodichka/metoda_matlogika_i_teor_algoritm_g6.html

V bibliografických katalozích	GND : 4343105-7