Hoares logik

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 15 juni 2021; kontroller kräver 2 redigeringar .

Hoare-logik ( eng.  Hoare-logik , även Floyd-Hoare-logik , eller Hoare-regler ) är ett formellt system med en uppsättning logiska regler utformade för att bevisa riktighet datorprogram . Den föreslogs 1969 av den engelske datavetaren och matematiska logikern Hoare , senare utvecklad av Hoare själv och andra forskare. [1] Den ursprungliga idén föreslogs av Floyd , som publicerade ett liknande system [2 ] som tillämpadesflödesscheman . 

Hoare trillingar

Det huvudsakliga kännetecknet för Hoares logik är Hoare - trippeln .  Trippeln beskriver hur exekveringen av en kodbit ändrar tillståndet för beräkningen. Hoare-trippeln har följande form:

där P och Q är påståenden och C är  ett kommando . _  _ P kallas förvillkoret ( antecedent ) och Q  kallas för eftervillkoret ( konsekvent ). Om förutsättningen är sann, gör kommandot postvillkoret sant. Påståenden är formler för predikatlogik .

Hoares logik har axiom och slutledningsregler för alla konstruktioner av ett enkelt imperativt programmeringsspråk . Utöver dessa konstruktioner som beskrivs i Hoares originalverk, utvecklade Hoare och andra regler för andra konstruktioner: samtidig exekvering , proceduranrop , hopp och pekare .

Hoares huvudidé är att ge varje konstruktion av ett imperativt språk ett för- och eftervillkor , skrivet som en logisk formel. Därför förekommer en trippel i namnet  - förutsättning , språkkonstruktion, postförutsättning .

Ett välfungerande program kan skrivas på många sätt, och i många fall blir det effektivt. Denna oklarhet komplicerar programmeringen. För att göra detta, introducera en stil. Men detta räcker inte. För många program (till exempel de som är indirekt kopplade till mänskligt liv) är det också nödvändigt att bevisa deras riktighet. Det visade sig att beviset på korrekthet gör programmet dyrare med en storleksordning (cirka 10 gånger).

Partiell och fullständig korrekthet

I Hoares standardlogik kan endast delvis korrekthet bevisas, eftersom programavslutning måste bevisas separat. Regeln att inte använda redundanta programdelar kan inte heller uttryckas i Hoares logik. Den "intuitiva" förståelsen av Hoare-trippeln kan uttryckas på följande sätt: om P inträffar innan C är fullbordat, så inträffar antingen Q eller kommer C aldrig att avslutas. Faktum är att om C inte avslutas, finns det ingen efter, så Q kan vara vilket påstående som helst. Dessutom kan vi välja att Q ska vara falskt för att visa att C aldrig kommer att avslutas.

Full korrekthet kan också bevisas med en utökad version av regeln för While -satsen .

Regler

Det tomma operatoraxiomet

Regeln för en tom sats säger att skip- satsen ( empty sats ) inte ändrar programmets tillstånd, så en sats som var sann innan skip förblir sann efter att den har körts.

Axiomet för tilldelningsoperatorn

Tilldelningsoperatorns axiom anger att efter en tilldelning ändras inte värdet av ett predikat med avseende på höger sida av tilldelningen när den högra sidan ersätts med vänster sida:

Här menas uttrycket P där alla förekomster av den fria variabeln x ersätts med uttrycket E .

Innebörden av uppdragsaxiomet är att sanningen är likvärdig efter att uppdraget har utförts. Således, om det var sant före tilldelningen, kommer det enligt tilldelningens axiom att vara sant efter tilldelningen. Omvänt, om det var lika med "falskt" före uppdraget, borde det vara lika med "falskt" efter.

Exempel på giltiga trippel:

Tilldelningsaxiomet i Hoares formulering gäller inte när mer än en identifierare hänvisar till samma värde. Till exempel,

är falskt om x och y refererar till samma variabel, eftersom ingen förutsättning kan säkerställa att y är 3 efter att x har tilldelats 2.

Regel för sammansättning

Hoares kompositionsregel gäller för sekventiell exekvering av programmen S och T , där S körs före T , som skrivs som S;T .

Tänk till exempel på två instanser av tilldelningens axiom:

och

Enligt kompositionsregeln får vi:

Villkorlig operatorregel

Inferensregel

Loop-satsregel

Här är P en cykelinvariant .

Cykelsatsregel med full korrekthet

I denna regel, förutom att bevara slinginvarianten, bevisas slingavslutning med en term som kallas slingvariabeln (här t ), vars värde strikt reduceras enligt den välgrundade relationen " < " med varje iteration. I det här fallet måste villkor B innebära att t inte är minimielementet i dess domän, annars kommer premissen för denna regel att vara falsk. Eftersom " < "-relationen är fullt välgrundad, definieras varje slingsteg av minskande medlemmar av en finit linjärt ordnad uppsättning .

Beteckningen för denna regel använder hakparenteser, inte klammerparenteser, för att indikera regelns fullständiga korrekthet. (Detta är ett sätt att beteckna fullständig korrekthet.)

Exempel

Exempel 1
— baserat på tilldelningens axiom.
Eftersom , baserat på slutledningsregeln, får vi:
Exempel 2
— baserat på tilldelningens axiom.
Om x och N är heltal, då , och baserat på slutledningsregeln, får vi:

Se även

Länkar

  1. BIL Hoare . " En axiomatisk grund för datorprogrammering Arkiverad 17 juli 2011 på Wayback Machine ". Communications of the ACM , 12(10):576-580,583 oktober 1969. doi : 10.1145/363235.363259
  2. RW Floyd . « Tilldela ord till program. Arkiverad från originalet den 9 december 2008.  (nedlänk sedan 2013-05-13 [3444 dagar] - historia ) »  (nedladdad länk) Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, sid. 19-31. 1967.

Litteratur