Ontwerp van Algoritmen 1: Checklist

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

  1. 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:
  2. De pre-post-bewijsverplichting bij catenatie S;T luidt
    Er bestaat een predikaat P met {preS {P} en {PT {post}
  3. Als statements in een programma genest zijn, moet je hun pre- en postcondities afleiden uit de context.
  4. Voor elke do-od-lus is eindiging een bewijsverplichting: 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
  5. Voor elke expressie E in een statement is (goede) gedefinieerdheid een bewijsverplichting: [ pre => def.E ]
  6. Bewijsverplichtingen voor binnenblokken zijn niet apart behandeld.
  7. Op bovenstaande manier zijn Hoare-triples geëlimineerd uit alle bewijsverplichtingen, eventueel m.u.v. afname bij eindiging van do-od.
  8. 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

  1. Laat duidelijk het verschil blijken tussen dat wat te bewijzen is en het bewijs zelf.
  2. Houd de redactie zo overzichtelijk mogelijk
  3. Maak verstandig gebruik van contexten. Schrijf bewijs voor [ P => Q ] i.h.a. op als
    |[ P
    |>
       Q
    ...
       true
    ]|
  4. Splits, waar mogelijk, bewijzen in onafhankelijke delen. Bijv. te bewijzen [ P => Q /\ R ]. Splits in [ P => Q ] en [ P => R ].
  5. Reken bij invarianten van de vorm x=phi.n niet met de hele invariant, maar alleen met phi.n.
  6. 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

  1. Conjunct weglaten uit postconditie
  2. Constante door variabele vervangen in postconditie
  3. Boven- en/of ondergrenzen op programmavariabele geven
  4. 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
  5. Staartinvariant van de vorm A=E waarbij constante A het te berekenen antwoord is en E een expressie is in termen van de programmavariabelen.
  6. Herschrijf eventueel eerst de postconditie (denk aan formule-vel)
  7. Introduceer geschikte afkortingen voor (deel)expressies in een invariant
  8. 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

  1. Geef formele specificatie
  2. Kies oplossingsstrategie; zoek bij repetitie een invariant
  3. Controleer finalisatie; kies geschikte guard; soms is er nog een statement na de repetitie nodig
  4. Zorg voor initialisatie; meestal is er een statement vóór de repetitie nodig; dit zou weer een (eenvoudigere) repetitie kunnen zijn
  5. Kies variante functie en verlagend statement; ontwerp body die invariant handhaaft (invariantie)
  6. Geef eindigingsbewijs
  7. Schrijf geannoteerde programma op
N.B. Sla geen stappen over.

Standaard phi-programma

  1. Dit is van toepassing op een probleem ter berekening van phi.N, met variatie van constante.
  2. 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 }
  3. 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.
  4. 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.
  5. 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: Het is wel nodig te vermelden

Invariant versterken

  1. 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.
  2. 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: Met name finalisatie en eindiging zijn niet meer nodig.
  3. 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.
  4. Zie ook de complicatie onder punt 4 van het standaard phi-programma.

Hulplussen

  1. 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.
  2. Voor een hulplus dient het hele stappenplan separaat afgehandeld te worden. Elke hulplus heeft dus zijn eigen
  3. Let er bij hulplussen op
  4. Een hulplus in de body van de hoofdlus wordt wel een binnenlus genoemd.
  5. 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

  1. 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.
  2. Leid voor die functie recurrente betrekkingen af. (Tot zover hetzelfde als het phi-schema.)
  3. 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).

  4. 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.
  5. 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.
  6. Construeer nu, volgens recept (zie onder), de code van het programma.
  7. Geef tenslotte het eindigingsbewijs.

Staartrecursieve recurrente betrekkingen

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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

  1. 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.
  2. 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.
  3. 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: Het is altijd nodig de volgende zaken expliciet te vermelden: Maar daarmee krijg je de volgende zaken kado: Essentieel om verder nog te presenteren zijn: N.B. Bij afwijken van dit patroon, dient met expliciet alle relevante bewijsverplichtingen na te komen. Dit doet zich bijvoorbeeld voor als

Zie ook The Binary Search Revisited (AvG127/WF214, 1995) door Netty van Gasteren en Wim Feijen.


Feedback about this page is welcome