Hoares logik

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 15. juni 2021; checks kræver 2 redigeringer .

Hoare-logik ( eng. Hoare-logik , også Floyd-Hoare-logik eller Hoare-regler ) er et formelt system med et sæt logiske regler designet til at bevise rigtigheden computerprogrammer . Det blev foreslået i 1969 af den engelske datalog og matematisk logiker Hoare , senere udviklet af Hoare selv og andre forskere. [1] Den oprindelige idé blev foreslået af Floyd , som udgav et lignende system [2 ] anvendt på flowcharts .

Hoare trillinger

Det vigtigste kendetegn ved Hoares logik er Hoare - trippelen . Trippelen beskriver, hvordan udførelsen af et stykke kode ændrer beregningens tilstand. Hoare triplen har følgende form:

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

hvor P og Q er påstande og C er en kommando _ _ _ P kaldes forudsætningen ( antecedent ) og Q kaldes postbetingelsen ( konsekvent ). Hvis forudsætningen er sand, gør kommandoen postbetingelsen sand. Udsagn er formler for prædikatlogik .

Hoares logik har aksiomer og slutningsregler for alle konstruktionerne af et simpelt imperativt programmeringssprog . Ud over disse konstruktioner beskrevet i Hoares originale arbejde, udviklede Hoare og andre regler for andre konstruktioner: samtidig udførelse , procedurekald , hop og pointer .

Hoares hovedidé er at give hver konstruktion af et imperativt sprog en præ- og postbetingelse , skrevet som en logisk formel. Derfor optræder en tredobbelt i navnet - forudsætning , sprogkonstruktion, postbetingelse .

Det er klart, at for en tom operatør er præ- og efterbetingelserne sammenfaldende.
For en tildelingsoperatør i en postcondition skal der udover forudsætningen tages hensyn til, at værdien af variablen er ændret.
For et sammensat udsagn (i Python er det indrykning, i C er det {} ) har vi en kæde af præ- og efterbetingelser . Som et resultat kan den første forudsætning og den sidste postbetingelse efterlades til den sammensatte sætning .
Inferensreglen siger, at vi kan styrke forudsætningen og svække postbetingelsen, hvis vi har brug for det. Det giver ingen mening at beholde hele programmet en form for erklæring, der ikke hjælper med at løse problemet.
Filialerklæring eller bare hvis . Det kan betinget opdeles i to grene: derefter og andet . Hvis vi tilføjer sandheden af den logiske betingelse til forudsætningen (hvad der er under if ), så efter udførelsen af den daværende gren , bør postbetingelsen følge . På samme måde, hvis vi tilføjer negationen af en logisk betingelse til forudsætningen (hvad er under if ), så efter udførelsen af else -grenen , bør postbetingelsen følge
sløjfeoperatør. Dette er det mest ikke-trivielle og komplekse, da løkken kan udføres mange gange og ikke engang slutte. For at løse problemet med mulig gentagen gentagelse af løkkelegemet introduceres løkkeinvarianten . En sløjfe-invariant er noget, der er sandt, før det udføres, er sandt efter hver udførelse af løkkelegemet og er derfor sandt efter slutningen af løkken. Forudsætningen for en loop-sætning er simpelthen dens loop-invariant . Hvis løkkefortsættelsesbetingelsen er sand (hvad er under while ), så efter udførelsen af løkkelegemet, bør sandheden af løkkeinvarianten følge . Som følge heraf har vi efter afslutningen af cyklussen som en postbetingelse sandheden af cyklusinvarianten og negationen af betingelsen for at fortsætte cyklussen.
Sløjfeoperatør med fuld korrekthed. For at gøre dette tilføjes en begrænsende funktion til det foregående afsnit, ved hjælp af hvilken det er nemt at bevise, at løkken vil blive udført et begrænset antal gange. Der stilles betingelser for den, at den altid er >=0, falder strengt efter hver udførelse af sløjfelegemet og nøjagtigt = 0, når sløjfen slutter.

Et velfungerende program kan skrives på mange måder, og det vil i mange tilfælde være effektivt. Denne tvetydighed komplicerer programmering. For at gøre dette skal du introducere en stil. Men det er ikke nok. For mange programmer (for eksempel dem, der indirekte er forbundet med menneskeliv), er det også nødvendigt at bevise deres rigtighed. Det viste sig, at beviset for rigtigheden gør programmet dyrere med en størrelsesorden (ca. 10 gange).

Delvis og fuld korrekthed

I Hoares standardlogik kan kun delvis korrekthed bevises, da programafslutning skal bevises særskilt. Reglen om ikke at bruge redundante programdele kan heller ikke udtrykkes i Hoares logik. Den "intuitive" forståelse af Hoare-trippelen kan udtrykkes som følger: hvis P forekommer før C er fuldført, så opstår enten Q , eller C vil aldrig ophøre. Faktisk, hvis C ikke afsluttes, er der ingen efter, så Q kan være et hvilket som helst udsagn. Desuden kan vi vælge Q til at være falsk for at vise, at C aldrig vil afslutte.

Fuld korrekthed kan også bevises ved at bruge en udvidet version af reglen for While- sætningen .

Regler

Det tomme operatoraksiom

Reglen for en tom sætning siger, at skip -sætningen ( empty statement ) ikke ændrer programmets tilstand, så en sætning, der var sand før skip , forbliver sand, efter at den er udført.

{\displaystyle {\frac {}{\{P\}\ {\textbf {spring over}}\ \{P\))))

Aksiomet for tildelingsoperatoren

Tildelingsoperatorens aksiom siger, at efter en tildeling ændres værdien af et hvilket som helst prædikat i forhold til højre side af opgaven ikke ved udskiftning af højre side med venstre side:

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

Her betyder udtrykket P , hvor alle forekomster af den frie variabel x er erstattet af udtrykket E . $P[E/x]$

Betydningen af opgaveaksiomet er, at sandheden er ækvivalent efter opgaven er udført. Hvis det således var sandt før opgaven, vil det ifølge opgaveaksiomet være sandt efter opgaven. Omvendt, hvis det var lig med "falsk" før opgaveerklæringen, skulle det være lig med "falsk" efter. $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$

Eksempler på gyldige tripler:

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

Tildelingsaksiomet i Hoares formulering gælder ikke, når mere end én identifikator refererer til samme værdi. For eksempel,

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

er falsk, hvis x og y refererer til den samme variabel, da ingen forudsætning kan sikre, at y er 3 efter x er blevet tildelt 2.

Reglen for sammensætning

Hoares kompositionsregel gælder for sekventiel afvikling af programmerne S og T , hvor S udføres før T , som skrives som S;T .

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

Overvej f.eks. to forekomster af opgaveaksiomet:

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

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

I henhold til sammensætningsreglen får vi:

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

Betinget operatorregel

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

Inferensregel

{\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 }}

Loop statement regel

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {mens}}\ B\ {\textbf {do}}\ S \ {\textbf {færdig}}\ \{\neg B\wedge P\}}}

Her er P en cyklusinvariant .

Cyklusudsagnsregel med fuld korrekthed

{\frac {<\;{\text{er velbegrundet,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P] \ {\textbf {mens}}\ B\ {\textbf {do}}\ S\ {\textbf {færdig}}\ [\neg B\wedge P]}}

I denne regel, ud over at bevare sløjfeinvarianten, bevises sløjfeterminering med et udtryk kaldet sløjfevariablen (her t ), hvis værdi er strengt reduceret i henhold til den velbegrundede relation " < " med hver iteration. I dette tilfælde skal betingelse B indebære, at t ikke er minimumselementet i dets domæne, ellers vil præmissen for denne regel være falsk. Fordi " < "-relationen er fuldt ud velbegrundet, er hvert sløjfetrin defineret af faldende medlemmer af et endeligt lineært ordnet sæt .

Notationen af denne regel bruger firkantede parenteser, ikke krøllede parenteser, for at angive reglens fuldstændige korrekthed. (Dette er en måde at betegne fuldstændig korrekthed på.)

Eksempler

Eksempel 1

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

— baseret på opgavens aksiom.

Da , baseret på inferensreglen, får vi:

( x + 1 = 43 \ Venstrehøjrepil x = 42 )

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

Eksempel 2

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