Brontekst bekijken van Beweren en bewijzen/de opzet/werkstuk/de opbouw

{{aanwijzing|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 ==

{{aanwijzing|''De inleiding en conclusie schrijf je als laatste, niet eer je weet wat in te leiden is.''}}

== Focus ==

=== Het doel ===
{{aanwijzing|Betreft het een demonstratiemodel, constructiemodel of verificatiemodel?}}

=== Het bestudeerde fragment van de realiteit ===

{{aanwijzing|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 ===
{{aanwijzing|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? ===

{{aanwijzing|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? ===

{{aanwijzing|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 ===

{{aanwijzing|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 ==

{{aanwijzing|De volgende drie secties moeten terminologisch precies bij elkaar passen.}}

=== Functioneel netwerk ===

{{aanwijzing|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 ===

{| class="wikitable"
! 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 ===

{{aanwijzing|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.}}

{| class="wikitable"
|-
! colspan="5" | Types
|-
! naam
! 
! betekenis
! 
! 
|-
| ...
| 
| 
| 
| 
|-
! colspan="5" | Functies
|-
! naam
! type
! betekenis
! 
! afk.*
|-
| ...
| 
| 
| 
| 
|-
! colspan="5" | Predikaten
|-
! naam
! type
! betekenis
! meting
! afk.*
|-
| ...
| 
| 
| 
| 
|}



{{aanwijzing|
Het is goed gebruik, fenomen die zich alleen onderscheiden door hun plaats en moment samen te vatten tot één predikaat:
;tijd&nbsp;: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&nbsp;: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.}}


{{aanwijzing|<nowiki>*)</nowiki> 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 ===

{{aanwijzing|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 ==

{{aanwijzing|'''Dit hoofdstuk moet precies passen bij het vorige.'''}}

=== {{aanwijzing|Per onderdeel}} ===

{{aanwijzing|
*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 &forall; en &rarr;)
*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")?}}

{{aanwijzing|Voorbeeld:}}

{{aanwijzing|<pre>Definition BEL := (forall t: T, stroom t) -> (forall t: T, druk t knop1 -> rinkel t).</pre> 
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&nbsp;:Gebruiksaanwijzing van de bel.
}}

== De specificatie van het geheel ==

{{aanwijzing|
* specificatie als naamgeving, leesbaar opgemaakt volgens de grammatica van onze taal
* verwoording van dezelfde specificatie in natuurlijke taal
}}

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

== De correctheidsstelling ==


{{aanwijzing|
* stelling als naamgeving, leesbaar opgemaakt volgens de grammatica van onze taal
}}

== Het bewijs ==

{{aanwijzing|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.}}
{|class="wikitable collapsible collapsed"
|-
! Coq-script
|-
|
<source lang="coq">
Require Import BenB.
...
</source>
|}

== Conclusie ==

{{aanwijzing|
''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?
}}