Predikativ programmering

Predikativ programmering är det ursprungliga namnet på en formell metod för programspecifikation och förfining , på senare tid kallad Practical Theory of Programming, uppfunnen av Eric Hehner . Den centrala idén är att varje specifikation är ett binärt ( booleskt ) uttryck som är sant för acceptabelt datorbeteende och falskt för oacceptabelt beteende. Av detta följer att förfining bara är implikation . Detta är den enklaste formella metoden, och den mest allmänna, som gäller för sekventiella, parallella, fristående, kommunicerande, avslutande, icke-avslutande, naturliga tid, realtid, deterministiska och probabilistiska program, och inkluderar tids- och rumsgränser .

Kommandon i ett programmeringsspråk anses vara ett specialfall av specifikation – de specifikationer som är kompilerbara. Till exempel, om programvariablerna är $x$ , $y$ och $z$ , är kommandot $x$ := $y$ +1 ekvivalent till specifikationen (binärt uttryck) $x'$ = $y$ +1 ∧ $y'$ = $y$ ∧ $z'$ = $z$ där $x$ , $y$ och $z$ representerar värdena för programvariablerna före tilldelningen, och $x'$ , $y'$ och $z'$ representerar värdena för programvariablerna efter tilldelningen. Om specifikationen är $x'$ > $y$ bevisar vi enkelt ( $x$ := $y$ +1) ⇒ ( $x'$ > $y$ ), som säger att $x$ := $y$ +1 innebär, eller förfinar, eller implementerar $x'$ > $y$ .

Slingbevis är mycket förenklat. Till exempel, om $x$ är en heltalsvariabel, för att bevisa det

medan $x$ >0 gör $x$ := $x$ –1 od

förfinar, eller implementerar specifikationen $x$ ≥0 ⇒ $x'$ =0, bevisa

om $x$ >0 då $x$ := $x$ –1; ( $x$ ≥0 ⇒ $x'$ =0) else $ok$ fi ⇒ ( $x$ ≥0 ⇒ $x'$ = 0)

där $ok$ = ( $x'$ = $x$ ) är det tomma, eller gör-ingenting-kommandot. Det finns inget behov av en loopinvariant eller minst fixpunkt . Slingor med flera mellanliggande grunda och djupa utgångar fungerar på samma sätt. Denna förenklade form av bevis är möjlig eftersom programkommandon och specifikationer kan blandas ihop på ett meningsfullt sätt.

Exekveringstid (övre gränser, nedre gränser, exakt tid) kan bevisas på samma sätt, bara genom att introducera en tidsvariabel. För att bevisa uppsägning, bevisa att exekveringstiden är begränsad. För att bevisa icke-uppsägning, bevisa att exekveringstiden är oändlig. Till exempel, om tidsvariabeln är $t$ och tiden mäts genom att räkna iterationer, då för att bevisa att exekvering av föregående while -loop tar tid $x$ när $x$ är initialt icke-negativ, och tar för evigt när $x$ initialt är negativ, bevisa

om $x$ >0 då $x$ := $x$ –1; $t$ := $t$ +1; ( $x$ ≥0 ⇒ $t'$ = $t$ + $x$ ) ∧ ( $x$ <0 ⇒ $t '$ =∞) else $ok$ fi ⇒ ( $x$ ≥0 ⇒ $t'$ = $t$ + $x$ ) ∧ ( $x$ <0 ⇒ $t'$ =∞)

där $ok$ = ( $x'$ = $x$ ∧ $t'$ = $t$ ).

Bibliografi

• ECR Hehner, a Practical Theory of Programming , Springer-Verlag 1993. Senaste upplagan online på a Practical Theory of Programming .

externa länkar

• Publikationer av Eric Hehner .