Zie ook de
toets
van feb. 2003 met
uitwerking
en
nakijkaanwijzingen.
N.B. Het gaat niet alleen om de vakkennis:
de theorie kennen.
Met name het kunnen toepassen er van is van belang.
Een belangrijk onderdeel hierbij is
de redactie van oplossingen:
hoe een oplossing op te schrijven en toegankelijk te presenteren.
Dit vergt (veel) oefening.
Bewijsverplichtingen en bewijzen
Bewijsverplichtingen vinden
- Voor elk statement in een programma is er een
bewijsverplichting die samenhangt met de preconditie pre
en postconditie post van het statement;
de rol van pre- en postconditie in die bewijsverplichting
hangt af van het soort statement:
- skip:
[ pre => post ]
- assignment S (substitutie):
[ pre => post(S) ]
- if-fi selectie:
[ pre => disjunctie van de guards ]
- do-od repetitie met als preconditie de invariant inv:
[ inv /\ not (disjunctie van de guards) => post ]
(eindiging is verderop vermeld)
- De pre-post-bewijsverplichting bij catenatie S;T
luidt
Er bestaat een predikaat P met
{pre} S {P} en
{P} T {post}
- Deze bewijsverplichting kom je i.h.a. meteen na door een
geschikt tussenpredikaat expliciet te vermelden en te gebruiken
in de bewijsverplichtingen voor S en T
(zie ook volgende punt).
- Vaak is het handig een naam aan het tussenpredikaat te geven.
- Meestal volstaat als tussenpredikaat de zwakste
preconditie van T bij postconditie post.
- Als statements in een programma genest zijn,
moet je hun pre- en postcondities afleiden uit de context.
- catenatie
{pre}
S;T
{post}
met tussenpredikaat P geeft
- if-fi-selectie
{pre}
if guard -> S [] ... fi
{post}
geeft
- {pre /\ guard} S {post}
- ...
- do-od-repetitie
{inv: inv}
do guard -> S [] ... od
{post}
geeft
- {inv /\ guard} S {inv}
- ...
- Voor elke do-od-lus is eindiging een bewijsverplichting:
- Vermeld variante functie vf
- Begrensdheid:
[ inv /\ disjunctie van de guards => 0=<vf]
- Afname in elk alternatief guard -> body:
{ inv /\ guard /\ vf=C } body { vf<C }
N.B. Als de afname in het alternatief bewerkstelligd wordt door maar
één assignment S,
d.w.z. de andere statements in het alternatief veranderen vf niet,
dan schrijven we de bewijsverplichting voor afname ook wel meteen als
- [ inv /\ guard => vf(S) < vf ]
- Voor elke expressie E in een statement is
(goede) gedefinieerdheid een bewijsverplichting:
[ pre => def.E ]
- Deze vermelden we i.h.a. alleen als gedefinieerdheid in het geding is,
bijv. bij array-indexering en deling (div, mod).
- Expressies kunnen voorkomen in assignments en
in guards van if-fi-selecties en do-od-repetities.
- Bewijsverplichtingen voor binnenblokken zijn niet apart behandeld.
- Op bovenstaande manier zijn Hoare-triples geëlimineerd
uit alle bewijsverplichtingen,
eventueel m.u.v. afname bij eindiging van do-od.
- Alle tussenpredikaten, invarianten en variante functies kunnen het
best vermeld worden in een geannoteerd programma.
Afgeleide pre-postcondities (zie punt 3)
voor geneste statements hoeven daarbij niet vermeld te worden
(maar bij diepere nesting is het vaak verstandig ze wel op te nemen).
Bewijzen opschrijven
- Laat duidelijk het verschil blijken
tussen dat wat te bewijzen is en het bewijs zelf.
- Houd de redactie zo overzichtelijk mogelijk
- Maak verstandig gebruik van contexten.
Schrijf bewijs voor [ P => Q ] i.h.a. op als
|[ P
|>
Q
...
true
]|
- Splits, waar mogelijk, bewijzen in onafhankelijke delen.
Bijv. te bewijzen [ P => Q /\ R ].
Splits in [ P => Q ] en [ P => R ].
- Reken bij invarianten van de vorm x=phi.n niet met de hele invariant,
maar alleen met phi.n.
- Reken bij (staart)invarianten van de vorm G.x.y=C niet met de hele
invariant, maar alleen met G.x.y.
Ontwerptechnieken
Invariant vinden
- Conjunct weglaten uit postconditie
- Constante door variabele vervangen in postconditie
- Boven- en/of ondergrenzen op programmavariabele geven
- Versterken met verse variabele:
Verse programmavariabele v introduceren en
de invariant versterken met conjunct van de vorm v=E,
waarbij E een expressie is in termen van de (andere)
programmavariabelen
- Staartinvariant van de vorm A=E
waarbij constante A het te berekenen antwoord is en
E een expressie is in termen van de programmavariabelen.
- Herschrijf eventueel eerst de postconditie (denk aan formule-vel)
- Introduceer geschikte afkortingen voor (deel)expressies in
een invariant
- Conjuncten uit de preconditie van de specificatie
die betrekking hebben op constanten
hoeven niet opgenomen te worden in een invariant
en kunnen overal gebruikt worden.
Stappenplan voor ontwerp van een repetitie
- Geef formele specificatie
- Kies oplossingsstrategie;
zoek bij repetitie een invariant
- Controleer finalisatie;
kies geschikte guard;
soms is er nog een statement na de repetitie nodig
- Zorg voor initialisatie;
meestal is er een statement vóór de repetitie nodig;
dit zou weer een (eenvoudigere) repetitie kunnen zijn
- Kies variante functie en verlagend statement;
ontwerp body die invariant handhaaft
(invariantie)
- Geef eindigingsbewijs
- Schrijf geannoteerde programma op
N.B. Sla geen stappen over.
Standaard phi-programma
- Dit is van toepassing op een probleem ter berekening van phi.N,
met variatie van constante.
- Het standaard phi-programma ziet er als volgt uit:
{ 0 =< N }
"x := phi.0" ; n := 0
; { inv: 0 =< n =< N /\ x = phi.n } { vf: N - n }
do n<>0 ->
"x := phi.(n+1)"
; { x = phi.(n+1) }
n := n + 1
od
{ x = phi.N }
- Te berekenen zijn phi.0 (initialisatie),
phi.(n+1) (invariantie).
Dit levert i.h.a. een recurrente betrekking voor functie phi,
waarbij phi.(n+1) is uitgedrukt in termen van phi.n.
Reken niet aan de gehele invariant.
- Een complicatie kan zich voordoen wanneer phi.(n+1)
niet (eenvoudig) te herschrijven is tot phi.n.
Dit wordt vaak veroorzaakt doordat n op meer plaatsen in
phi.n voorkomt.
Bijvoorbeeld
phi.n = (E i: 0 =< i < n: f.i < f.n)
In zo'n geval is het aan te raden om eerst phi.n te
herschrijven en de invariant aan te passen of te versterken.
In dit voorbeeld:
phi.n = (min i: 0 =< i < n: f.i) < f.n
Houd nu bij
psi.n = (min i: 0 =< i < n: f.i)
en neem in de body
x := psi.(n+1) < f.(n+1)
Het is dan niet meer nodig phi.n bij te houden.
- Variaties hierop betreffen een andere beginwaarde voor n
en een andere looprichting n:=n-1.
I.h.a. hoeven bij phi-programma's de volgende zaken
niet expliciet bewezen te worden:
- Finalisatie bij guard n<>N .
- Initialisatie en invariantie van de grenzen 0=<n=<N .
- Terminatie (begrensdheid en voortgang).
Het is wel nodig te vermelden
- wat de invarianten zijn;
- wat de variante functie is.
Invariant versterken
- Een expressie E die in het programma nodig is
maar daar niet bruikbaar is
(verboden is, geen programma-expressie is, te langzaam is),
kan vervangen worden door een variabele v
mits ter plekke geldt v=E.
- Een manier om dit te realiseren is
de invariant versterken met P: v=E.
De volgende stappen uit het stappenplan dienen
voor de versterking opnieuw afgehandeld te worden:
- Initialisatie van P
- Invariantie van P
Met name finalisatie en eindiging zijn niet meer nodig.
- Let er op dat na afloop van de repetitie de invariant geldt.
Dit is problematisch als E dan niet gedefinieerd is.
Een manier om dat soms op te lossen is verschuiven.
Stel dat n:=n+1 het statement is dat de variante
functie verlaagt.
Versterk nu de invariant met P': v=F,
zodanig dat E=F(n:=n+1).
Bewerkstellig in de body eerst P'(n:=n+1)
en gebruik vervolgens v i.p.v. E.
- Zie ook de complicatie onder punt 4 van het
standaard phi-programma.
Hulplussen
- Indien bij het ontwerp van de body, initialisatie,
of naberekening van een repetitie (hier even hoofdlus genoemd)
een deelprobleem ontstaat dat men wil oplossen met een repetitie,
dan noemen we die repetitie een hulplus.
-
Voor een hulplus dient het hele
stappenplan separaat afgehandeld te worden.
Elke hulplus heeft dus zijn eigen
- specificatie (pre/post)
- invariant(en)
- finalisatie/guard
- variante functie
- voortgangmakende body die invariant handhaaft
- terminatiezorg
- Let er bij hulplussen op
- dat verse variabelen zo locaal mogelijk (in een eigen binnenblok)
gedeclareerd worden;
- dat deze variabelen niet in de invariant van de hoofdlus
vóórkomen;
- dat variabelen van de hoofdlus op gepaste wijze behandeld worden
in de hulplus (veelal: ongewijzigd blijven).
- Een hulplus in de body van de hoofdlus wordt wel een binnenlus
genoemd.
- I.h.a. zijn programma's met een binnenlus minder efficiënt
dan met een versterkte invariant.
N.B. Als het efficiënter kan en dat ook gevraagd is,
dan kan men voor een oplossing met binnelus wel een voldoende halen,
maar dat is dan iets als 6 van de 10 punten.
Staartinvarianten
Werkwijze bij staartinvariant
- Vervang in (het relevante deel van) de postconditie een
(of meer) constante(n) door een (of meer) variabele(n),
en verkrijg aldus een functie F.
- Leid voor die functie recurrente betrekkingen af.
(Tot zover hetzelfde als het phi-schema.)
- Als het phi-schema niet toepasbaar (b)lijkt,
generaliseer dan de functie F,
door te analyseren wat de verschillende betrekkingen
voor die functie gemeen hebben.
Dit is in de regel de lastigste stap in het proces.
Vaak helpt het om een concreet voorbeeld met de hand door
te rekenen.
Dit leidt tot een nieuwe functie G met
meer variabelen (i.e. parameters).
- Leid voor die nieuwe functie G recurrente betrekkingen af,
gebruikmakend van de betrekkingen voor de oude functie F.
Hierin zit wat werk maar het is voor veel opgaven niet echt moeilijk.
Het resultaat dient een staartrecursieve definitie
(zie hieronder) voor G te zijn.
- Kies de (standaard) staartinvariant en, zonodig, een extra
invariant ter begrenzing van (sommige) variabele(n).
Die staartinvariant kan op twee manieren worden opgeschreven:
in termen van G of van F;
beide zijn toegestaan.
- Construeer nu, volgens recept (zie onder), de code van het programma.
- Geef tenslotte het eindigingsbewijs.
Staartrecursieve recurrente betrekkingen
- Een recurrente betrekking voor functie G is
een stel gelijkheden van de vorm G.x.y.z=E,
waarbij de expressies E weer nul
of meer toepassingen van G bevatten.
Een gelijkheid met een rechterlid waarin G niet vóórkomt
heet een basisgeval.
- Een recurrente betrekking voor functie G is
volledig als voor elk relevant argumenttupel voor G
er een gelijkheid is waarbij het linkerlid van toepassing is
op dat argumenttupel.
- Een recurrente betrekking voor functie G is
consistent als voor elk relevant argumenttupel voor G
dat past bij meer dan één gelijkheid,
de bijbehorende rechterleden allemaal dezelfde waarde hebben.
- Een recurrente betrekking voor functie G is
goedgedefinieerd als deze volledig en consistent is en
bovendien voor elk argumenttupel dan van toepassing is voor G
de herschrijving via de recurrente betrekkingen termineert, d.w.z.
in een eindig aantal stappen leidt tot basisgevallen.
- Een recurrente betrekking voor functie G is
staartrecursief,
als de hoofdoperator van rechterleden E,
die geen basisgeval zijn,
de functie G zelf is, en bovendien
G verder niet vóórkomt in E.
Bijbehorende programma construeren
- De guard van de repetitie bestaat i.h.a. uit de disjunctie van
de condities die leiden tot niet-basisgevallen
(d.w.z. tot gevallen waarin sprake is van recursie).
Dit is gelijk aan de conjunctie van de ontkenningen van de condities
die leiden tot basisgevallen.
- In de basisgevallen (d.w.z. zodra de ontkenning van de guard geldt),
kan het zijn dat de postconditie nog niet gerealiseerd is,
maar dat hiervoor nog een naberekening nodig is.
- Zie verder Programming: The Derivation of Algorithms p. 73-74.
Zoeken
Linear Search
De Linear Search heeft zijn eigen stelling
(zie Programming: The Derivation of Algorithms, p.94).
Als je aantoont dat de stelling van toepassing is
(m.n. dat uit de gegeven preconditie volgt dat "het gezochte" bestaat),
dan kun je zonder verdere afleiding het programma opschrijven.
N.B. O.g.v. symmetrie is er ook de variant met max,
waarbij vanaf een bovengrens naar beneden gezocht wordt.
Zie ook (Bounded) Linear Search by Tail Recursion.
Bounded Linear Search
Zie Programming: The Derivation of Algorithms.
Binary Search
De Binary Search is niet zozeer een algoritme,
maar eerder een algoritme-patroon.
De ingredienten van dit patroon zijn:
- Invarianten (van de vorm):
P0: 0 =< x < y =< N
P1: P.x.y
- Variante functie: y - x
- Guard: x+1 <> y
- P.x.y is zodanig
- [initialisatie] dat P.0.N volgt uit de preconditie
(of eenvoudig daaruit te bewerkstelligen is),
eventueel m.b.v. geschikt gekozen denkelementen;
- [finalisatie] dat 0 =< x < N /\ P.x.(x+1)
de gewenste postconditie impliceert
(of dat daaruit de gewenste postconditie eenvoudig te bewerkstelligen is).
N.B.
Het is aan te bevelen om P.x.y eenvoudig te houden
(met zo min mogelijk kwantoren);
dit kan eventueel door de preconditie uit te buiten (mits die invariant is);
d.w.z. de preconditie speelt dan zijn voornaamste rol bij het argument voor
finalisatie: 0 =< x < N /\ P.x.(x+1) impliceert postconditie;
het voordeel is dat berekening van de if-guards
voor x := h en y := h
(zie hieronder) dan eenvoudiger zijn
- { 0 =< x < x+1 < y =< N }
h := (x + y) div 2
{ Q: 0 =< x < h < y =< N }
- Onderzoek toekenningen x := h en y := h om voortgang te maken;
bepaal guards Bx en By met
- Q /\ P.x.y /\ Bx impliceert P.h.y
- Q /\ P.x.y /\ By impliceert P.x.h
zodanig dat Bx \/ By geldt;
ga in die berekening uit van P.h.y resp. P.x.h en
gebruik Q /\ P.x.y om deze te vereenvoudigen tot een programma-expressies;
beroep u waar mogelijk op symmetrie
Het is altijd nodig de volgende zaken expliciet te vermelden:
- invarianten (denk aan de grenzen zoals boven in P0),
- variante functie (zoals boven),
- de postconditie Q na toekenning aan h (zoals boven).
Maar daarmee krijg je de volgende zaken kado:
- Correctheid van:
{ 0 =< x < x+1 < y =< N }
h := (x + y) div 2
{ Q: 0 =< x < h < y =< N }
- Invariantie van P0
- Eindiging, en wel in O(log N) iteraties
Essentieel om verder nog te presenteren zijn:
- Initialisatie en finalisatie (zijn i.h.a. eenvoudig)
- Bepaling van de if-guards (voor x := h en y := h)
- Gedefinieerdheid van expressies (m.n. die if-guards; gebruik Q)
- Disjunctie van de if-guards (hier kan de preconditie ook wel eens helpen)
N.B. Bij afwijken van dit patroon,
dient met expliciet alle relevante bewijsverplichtingen na te komen.
Dit doet zich bijvoorbeeld voor als
- de invariant x=<y bevat i.p.v. x<y ;
- de guard x<>y is i.p.v. x+1<>y ;
- voortgang gemaakt wordt met x:=h+1 i.p.v. x:=h .
Zie ook The Binary Search Revisited
(AvG127/WF214, 1995) door Netty van Gasteren en Wim Feijen.
Feedback about this page is welcome