Beweren en bewijzen/de opzet/werkstuk/spannend

Een werkstuk moet uiteraard voldoen aan de kwaliteitseisen. En uiteindelijk moet het bewijs van de correctheidsstelling kloppen. Maar, er zijn natuurlijk erg triviale voorbeelden te bedenken die aan al deze eisen voldoen. Dat maakt ze nog niet tot goede werkstukken!

Een werkstuk is "spannend" als de correctheidsstelling voldoende substantie heeft om aan te tonen dat je het vak beheerst. Om te kijken of je werkstuk spannend genoeg is kun je letten op de volgende dingen:

• Er moet predikaatlogica in voor komen. De predikaatlogica moet bovendien op een niet triviale manier worden gebruikt. Een eenvoudige manier (maar het kan ook op andere wijzen) is om tijd te introduceren. Het is dan onvoldoende om alle predikaten uit te breiden met een tijdsparameter t en vervolgens overall ∀ t:T voor te zetten. In dat geval zal in het bewijs enkel over één tijdstip t geredeneerd hoeven worden. De tijd speelt dan eigenlijk geen rol. Een oplossing is om vertragingen in onderdelen mee te nemen. Dat is zeker een goed idee, maar je zult meer moeten verzinnen om het spannend te maken. Dat komt omdat enkel vertragingen nog een vrij simpel geheel geven. Neem bijvoorbeeld de volgende simpele correctheidsstelling (ga na dat deze simpel te bewijzen is):

(∀ t:T, P t -> Q t+1),
(∀ t:T, Q t -> R t+2),
(∀ t:T, R t -> S t+4),
|-
(∀ t:T, P t -> S t+7)

• Kwantificatie over andere domeinen dan tijd kan ook, maar is vaak lastiger.
• Pas bij kwantificatie altijd op voor zinloze kwantificatie.
• Probeer iets met intervallen. In plaats van de exacte vertragingen in het bovenstaande voorbeeld kun je een paar onderdelen hebben waarbij de vertraging b.v. tussen 5 en 7 seconden is.
• Probeer iets met een onderdeel dat eerst gedurende een tijd `opgeladen` moet worden voordat het (goed) werkt. Denk aan een drukvat, verwarmingselement, o.i.d.
• Probeer iets met een timer. Een timer is een onderdeel dat wanneer het gestart wordt een afgebakende tijd een signaal geeft. De timer hoeft niet expliciet een onderdeel te zijn, je kunt ook onderdelen gebruiken die intern een timer hebben of gedrag vergelijkbaar aan een timer hebben. Bijvoorbeeld het Beweren_en_bewijzen/de_zuilen/Taal/6._Tijdslogica of de waterpomp in een koffiemachine die voldoende lang water pompt.
• Laat je inspireren door de interessante artefacten op Beweren_en_bewijzen/de_zuilen/Taal/2._Logica en Beweren_en_bewijzen/de_zuilen/Taal/6._Tijdslogica ook de casusen in het literatuur lijstje.
• Onderdelen moeten niet naadloos op elkaar aansluiten. Voorbeeld Definition onderdeel1 := P -> (een_hele_moeilijke _formule). en Definition onderdeel2 := (een_hele_moeilijke_formule) -> Q. De formule mag dan wel heel moeilijk zijn maar hij is in beide onderdelen hetzelfde en het zal geen verbazing wekken dat P → Q eenvoudig te bewijzen is.
• Er moeten voldoende onderdelen zijn.
• Je kunt het interessanter maken met een dozen in dozen benadering, waarbij je dus meerdere niveau's hebt. Op het hoogste niveau heb je een aantal onderdelen, hun specificatie en de specificatie van het geheel. Maar er is ook een onderdeel dat je uit kunt vouwen in subonderdelen.
• In sommige werkstukken is het heel belangrijk dat de gebuiker (dat kan ook een ander systeem zijn) het artefact op precies de juiste wijze gebruikt. Voorbeeld: eerst de kaas op de boterham doen, dan het geheel in het tosti-ijzer en vervolgens er op tijd uithalen. In zo'n geval wordt het een stuk interessanter als men de gebruiker als onderdeel van het systeem beschouwt. Voorbeeld: tosti-ijzer en Pietje zorgen tezamen, mits er voldoende kaas en boterhammen zijn, binnen 30 min voor een tosti.
• Je kunt natuurlijk zeer spannende onderdelen bedenken, maar uiteindelijk wordt het alleen spannender als deze onderdelen er ook toe doen: zonder het onderdeel kan het geheel niet aan haar specificatie voldoen.
• Maak het ook weer niet te moeilijk. Het moet in het tijdsbestek van het vak passen.