Beweren en bewijzen/kwaliteit

B0 De blauwdruk geeft aan uit welke onderdelen het artefact bestaat. Daartoe bevat de blauwdruk hetzij een specificatie van elk onderdeel hetzij een verwijzing naar een elders staande specificatie.
B1 De blauwdruk geeft aan welke onderdelen welke waarneembare fenomenen met elkaar delen (en daarmee de samenhang van de onderdelen).
B2 De blauwdruk bevat alle informatie die nodig is om de gewenste eigenschappen van het artefact te bewijzen.
B3 Voor dezelfde onderdelen en dezelfde fenomenen worden in een blauwdruk ook precies dezelfde woorden gebruikt.
B4 Een blauwdruk beschrijft niet zo veel onderdelen dat men het overzicht verliest. Mensen kunnen niet goed meer dan 7 dingen onderscheiden, dus kun je beter niet veel meer dan 7 onderdelen hebben.
B5 Algemeen bekende functionaliteit of standaard-onderdelen verdienen de voorkeur.
B6 Als ter ondersteuning van de leesbaarheid redundante informatie (bijvoorbeeld diagrammen, commentaren, formules) toegevoegd worden, dient het geheel consistent te zijn (zelfde aantal onderdelen, precies dezelfde namen).

^{Beweren en bewijzen/kwaliteit/domeinmodel}

Kwaliteitscriteria domeinmodel

D1. Belangrijk is dat voor elk predikaat in het domeinmodel een meting aangegeven is, waarmee je in de realiteit kunt nagaan of een predikaat waar is. In Beweren en Bewijzen houden we ons alleen bezig met beweringen, opgebouwd uit predikaten die met zo'n meting corresponderen.
D2. Een goed domeinmodel is minimaal, d.w.z. het bevat geen elementen die zich door definities laten samenstellen uit andere elementen van dit domeinmodel. (Als een domeinmodel bv. de predikaten 'is kind van' en 'is vrouwelijk' bevat, zijn de predikaten 'is zoon van' en 'is mannelijk' niet nodig, omdat ze zich laten definiëren.)
D3. Zorgvuldig en systematisch gekozen namen in het domeinmodel en bij eigen definities kunnen helpen verwarring te voorkomen.

^{Beweren en bewijzen/kwaliteit/focus}

Kwaliteitscriteria focus (afbakening van het doel van een ontwerp- of verificatievraagstuk en het behandelde fragment van de realiteit en perspectief)

F0 Er moet aangegeven zijn waartoe de exercitie dient: gaat het om het volledig beschrijven van een ding of alleen om het bewijzen van één eigenschap? (In Beweren en bewijzen gaat het doorgaans om het laatste. Je volstaat met een →verificatiemodel.)
F1 Het fragment van de wereld dat je wilt onderzoeken moet duidelijk afgebakend zijn en vastliggen. (In Beweren en bewijzen is dat doorgaans een →artefact dat een onderdeel van een groter systeem is.)
F2 Wat dynamisch is en wat als onveranderlijk beschouwd wordt, moet vastliggen. (In deze cursus zullen we computergestuurde systemen onderzoeken. We gaan er dan van uit dat het programma zelf en de hardware ongewijzigd blijft en alle kabeltjes op hun plek blijven.)
F3 Het perspectief, d.w.z. de te onderzoeken eigenschap van het fragment van de realiteit moet enigszins vastliggen. (In deze cursus gaat het vooral om gedrag van een dynamisch systeem.)
F4 Bij verificatievraagstukken (F0) praat je alleen over dingen en fenomenen die relevant zijn onder het gekozen perspectief.
F5 De nodige domeinkennis moet aanwezig zijn.
F6 Als je niet over één specifiek fragment van de wereld praat maar over een hele klasse, moet je goed weten hoe men dat doet.

^{Beweren en bewijzen/kwaliteit/geformaliseerde natuurlijke taal}

Kwaliteitscriteria geformaliseerde natuurlijke taal

Gebruik voor dezelfde dingen steeds precies dezelfde woorden. Gebruik verschillende woorden als signaal dat er een verschil in betekenis is.
Gebruik bij het maken van zinnen geen voegwoorden waarvan de betekenis vaag is. In de formele logica hebben alle voegtekens een precieze betekenis: ∧, ∨, → etc. In de natuurlijke taal gaat het met "of" al mis. Hoe beter je formele talen beheerst hoe preciezer je natuurlijke taal kunt toepassen, omdat de formele talen je de problemen duidelijk hebben gemaakt.
Maak absoluut duidelijk waar je een eigen begrip definieert en houd je dan precies aan deze definitie en gebruik de term daarna in de tekst nooit meer in de "gewone" betekenis.
Zeg geen woord te veel.
Vermijd modale woordjes als "kan", "moet", "mag".
Gebruik aanhalingstekens als je in de taal over de taal schrijft. "In het Nederlands" heeft zeker 15 letters. In het Nederlands heeft "zeker" 5 letters.
Gebruik verschillende lettertypes waar dat helpt verschillende taalniveaus te onderscheiden.

^{Beweren en bewijzen/kwaliteit/onze taal}

Kwaliteitscriteria onze taal

syntax
- conform de grammatica
- goed getypeerd
- alle variabelen gedeclareerd
semantiek
- de juiste quantoren op de juiste plaats
- bereik van quantoren klopt
opmaak
- liever geen overbodige haakjes
- regels niet te lang
- opmaak geeft syntactische structuur weer

^{Beweren en bewijzen/kwaliteit/opmaak van formules}

Kwaliteitscriteria opmaak van formules

Formules mogen nooit zo breed gezet worden dat ze van de pagina aflopen.
Een sluitend haakje staat
- óf op dezelfde regel als het bijbehorende openend haakje
- óf precies eronder.
Hetzelfde geldt voor voegtekens en operatoren op hetzelfde niveau.
Wees zuinig met onnodige haakjes en witruimte.

^{Beweren en bewijzen/kwaliteit/specificatie}

Kwaliteitscriteria specificatie

S0 Een specificatie is niet ambigu:
- Dit betreft allereerst eenduidige syntax. Als een bewering twee verschillende syntaxbomen kan hebben moeten deze tenminste dezelfde semantiek hebben.
- Geen knel: Dezelfde termen in een specificatie moeten absoluut dezelfde begrippen of fenomenen betekenen, ook al zijn deze misschien nog niet nader gedefinieerd.
S1 Een specificatie zegt kernachtig en onomwonden wat het geval is als het gespecificeerde ding - het fragment van de realiteit uit de focus - naar behoren functioneert.
- Een specificatie zegt niet dat ze een specificatie is
- en ook niet dat ze alleen geldt als het gespecificeerde ding niet kapot is.
- Een specificatie noemt het in de focus vastgelegde ding niet; dat is al in de focus genoemd. Ze noemt we de fenomenen die het ding met zijn omgeving deelt (zie onder S3).
- Modale hulpwerkwoorden ("kan", "mag", "moet") komen er niet in voor.
S2 Een specificatie gaat over het Wat, niet over het Hoe.
- De belangrijkste reden hiervoor is dat op deze manier geen alternatieven bij voorbaat worden uitgesloten. (Het Hoe betreft de onderdelen, die je in de blackbox view dus even niet ziet).
- Het is mogelijk naar een bekend Hoe te refereren om een bepaalde kwaliteit te specificeren ("hoorbare muziek alsof een strijkkwartet in de kamer speelt"), maar dan moet duidelijk zijn dat andere realisaties (bijvoorbeeld met luidsprekers) niet uitgesloten zijn (in dit voorbeeld door het woordje "alsof" aangegeven).
S3 Een specificatie specificeert uit een bepaald perspectief eigenschappen van een afgebakend fragment van de realiteiten juist niet diens omgeving.
- Hooguit maakt de specificatie expliciet aannames over de omgeving.
- Maar de specificatie moet alle voor het doel nodige informatie bevatten voor iemand die de omgeving van het gespecificeerde fragment van de realiteit niet kent.
- Een specificatie praat alleen over fenomenen die het te specificeren ding deelt met zijn omgeving.
S4 De specificatie van het gedrag van een ding specificeert welke scenario's kunnen gebeuren en welke uitgesloten zijn als het ding er is en naar behoren functioneert.
- Een gedragsspecificatie is een beschrijving van een verzameling van scenario's.
- Een scenario is een verzameling (afloop) van gebeurtenissen.
S5 De gebeurtenissen waarover specificaties praten zijn in ons vak "waarneembare fenomenen": iets waarvan men met een enkelvoudige observatie of meting kan vaststellen of het daadwerkelijk gebeurt of niet.
- Voorafgaand aan een specificatie dient een lijst van zulke fenomenen gegeven te worden
- waarbij bij elk fenomeen de meting aangegeven is
- en in de specificatie dezelfde fenomenen doorgaans hetzelfde genoemd worden.
- In de beschrijving van zo'n fenomeen komen in principe geen voegwoorden voor.
S6 Fenomenen mogen bewust (een tijdje) ondergespecificeerd blijven ("gecontroleerde vaagheid").
- D.w.z. je laat sommige begrippen nog een beetje "open" of "vaag" (een betere term is "kwalitatief", bijv. stroom) totdat je eraan toe bent ze optimaal precies te maken ("kwantitatief", bijv. 230V, 50 Hz, 10 mA).
- Onderspecificatie geldt vaak tijdens het specificatieproces, maar meestal niet meer aan het eind.