Beweren en bewijzen/de opzet/werkstuk/de opbouw

Je kunt de code van deze pagina kopiëren naar de werkstukpagina. Stap voor stap vervang je dan de grijze aanwijzingen door je eigen tekst.

Inleiding

De inleiding en conclusie schrijf je als laatste, niet eer je weet wat in te leiden is.

Focus

Het doel

Betreft het een demonstratiemodel, constructiemodel of verificatiemodel?

Het bestudeerde fragment van de realiteit

Om welk artefact gaat het? Wat hoort erbij, wat is de omgeving? Je mag hier ook een foto of een schets geven, maar alleen als deze echt iets toevoegt. Hoe een auto of een tandenborstel eruitziet, weten we.

Het gezichtspunt

Welke eigenschap wordt onderzocht? Geef een eerste benadering van een heldere specificatie van je artefact in natuurlijke taal. Maak duidelijk welke fenomenen het met zijn omgeving deelt, voor zover deze relevant zijn voor de onderzochte eigenschap.

Waarom?

Waarom juist dit onderwerp? Eventuele bedenkingen en afwegingen omtrent deze keuze. Welke domeinkennis is nodig? Is deze in de groep aanwezig? Achtergrondinformatie.

Wat wordt formeel behandeld?

Hier kun je aangeven welke eigenschappen je zo belangrijk vindt dat ze in de correctheidsstelling meegenomen moeten worden en welke je zo vanzelfsprekend of weinig interessant vindt dat je ervan abstraheert. Voorbeelden: voeding en koeling van elektronische apparatuur.

Vereenvoudigingen

Afhankelijk van de vraagstelling kunnen bepaalde simplificaties en idealiseringen legitiem zijn. Bij thuiselektronica mag je bijvoorbeeld aannemen dat de netspanning constant is, terwijl ze in werkelijkheid altijd wat schommelt. Tenzij je juist een overspanningsbeveiliging wilt behandelen. Bij veel besturingsproblemen kun je de rekentijd van de computer gerust verwaarlozen. Dat soort dingen noem je hier.

Structuur

De volgende drie secties moeten terminologisch precies bij elkaar passen.

Functioneel netwerk

Upload s.v.p. geen plaatjes met functionele netwerken; anders krijgen we hier honderden plaatjes met verouderde versies. Gebruik GraphViz! Teken onderdelen als blokjes en waarneembare fenomenen als lijnen. (Een pijl die je in de lucht wilt laten hangen kun je naar een onzichtbaar blokje laten gaan.)

Onderdelen

naam	korte informele specificatie
moet precies passen bij het functioneel netwerk	Eén heldere zin is hier voldoende. Zie het als toelichting van het functioneel netwerk. Gebruik precies de juiste woorden voor de gedeelde fenomenen! Neem de criteria ter harte.

Het domeinmodel

Eerst vul je naam, betekenis en meting in. De rest pas als je overgaat tot formalisering. De namen moeten wel precies passen bij het bovenstaande. Je mag wel fenomenen samenvatten, zoals onder de tabel uitgelegd.

Types
naam		betekenis
...
Functies
naam	type	betekenis		afk.*
...
Predikaten
naam	type	betekenis	meting	afk.*
...

Het is goed gebruik, fenomen die zich alleen onderscheiden door hun plaats en moment samen te vatten tot één predikaat:

tijd 

Bij real-timesystemen heeft elk predikaat een tijdsparameter: het moment waarop iets geobserveerd kan worden. Geef aan wat je tijdsmodel is. Reële getallen? Gehele getallen? Welke eenheid?

plaats 

Als gelijksoortige fenomenen zich op verschillende plekken in het systeem voordoen, kan een tweede parameter een locatie aangeven.

In elk geval moet de relatie tussen het domeinmodel en het functioneel netwerk voor de lezer in één oogopslag helder zijn.

*) Indien de namen van de predikaten en functies lang zijn, kun je d.m.v. afkortingen een voor Coq beter behapbare variant van de correctheidsstelling schrijven. Gebruik leesbare namen voor optimale leesbaarheid voor de specificaties en het netwerk en zeer korte afkortingen voor een versie van je correctheidsstelling die nog op een Coq-scherm past.

Hulpdefinities

Optioneel. Samengestelde predikaten, gedefinieerd op basis van de predikaten uit het domeinmodel. Geef niet alleen de formules, maar leg ook uit in natuurlijke taal wat het nut is van die formules.

Onderdeelspecificaties

Dit hoofdstuk moet precies passen bij het vorige.

Per onderdeel

• de naam
• specificatie als naamgeving, leesbaar opgemaakt volgens de grammatica van onze taal (deze formele specificatie moet uiteindelijk precies overeenkomen met die in het Coq-script, dus gebruik ASCII-notaties als 'forall' en '->' in plaats van ∀ en →)
• verwoording van dezelfde specificatie in natuurlijke taal
• eventueel extra uitleg, keuzes, afwegingen
• korte verantwoording: hoe kun je nagaan of deze specificatie in het echt juist is ("verificatie")?

Voorbeeld:

Definition BEL := (forall t: T, stroom t) -> (forall t: T, druk t knop1 -> rinkel t).

De bel rinkelt zolang knop1 ingedrukt is. Alles onder de voorwaarde dat er de hele tijd stroom is.

afweging

Er zijn ook bellen die alleen stroom nodig hebben zolang de knop ingedrukt is. De "kleine a" is hier bewust breder gehouden om geen bellen uit te sluiten waar een computer in zit.

verificatie 

Gebruiksaanwijzing van de bel.

De specificatie van het geheel

• specificatie als naamgeving, leesbaar opgemaakt volgens de grammatica van onze taal
• verwoording van dezelfde specificatie in natuurlijke taal

Dit moet natuurlijk aansluiten bij de eerste specificatie in natuurlijke taal in het begin van het werkstuk.

De correctheidsstelling

• stelling als naamgeving, leesbaar opgemaakt volgens de grammatica van onze taal

Het bewijs

Voeg hier het complete Coq-script toe in een inklapbare en ook ingeklapte tabel, zodat met een simpele kopieer- en plakactie het bewijs in Coq te controleren is, maar er bij een afdruk van dit werkstuk geen papier aan het bewijs wordt verspild.

Coq-script
<source lang="coq"> Require Import BenB. ... </source>

Conclusie

De inleiding en conclusie schrijf je als laatste, niet eer je weet wat te concluderen is.

• Is het gelukt om het bewijs af te ronden of ben je tegen een probleem aangelopen?