Beweren en bewijzen/supplement/planning (voor docenten)/het werk/taak/08

Beweren en bewijzen: "redeneren op het hoogste niveau over gemaakte dingen". We beheersen nu de taal van de predikaatlogica en weten hoe we domeinmodellen en hulpdefinities maken. Nu zetten we de puntjes op de i en brengen het geleerde in de praktijk van de systeemontwikkeling.

Achtergrond

Deze taak is tegelijk de 3e mijlpaal. Het is niet iets wat je even op een late zondagavond maakt. Je hebt tijd en afstemming met je groepsgenoten nodig. Let op de veranderde deadline: de uitwerkingen moet nu op maandag al om 9:00 in de werkplaats staan. In de loop van maandagochtend wordt de indeling voor de responsiecolleges bekend gemaakt. Als het even kan, gaan we naar sessies van twee uur.

Aan de hand van de Beweren en bewijzen/het verhaal/4. De taal/oefenpagina controleer je een laatste keer of je nu de taal en met name het gebruik van quantoren beheerst. Als het goed is ken je dan voldoende predikaatlogica om de specificaties in het werkstuk te kunnen maken.

Doel

literatuur Gebruiker:Hanno Wupper/voorbeeld 6. Tijd

• Je kunt een predikaatlogisch domeinmodel maken voor real-timesystemen.
• Je kunt specificaties van artefacten in predikaatlogica en in natuurlijke taal opstellen
• en structureren m.b.v. hulpdefinities.
• Je kunt de syntaxis van je specificaties en hulpdefinities laten controleren door een bewijsassistent.

Instructie

1. Bekijk nog eens goed het voorbeeld op Gebruiker:Hanno Wupper/voorbeeld. Hier zie je hoe positie en bereik van quantoren systematisch afgeleid worden tijden de vertaling van een bewering.
2. Verbeter nu, indien van toepassing, één foute definitie of bewering op Beweren en bewijzen/het verhaal/4. De taal/oefenpagina.
   • Bij een aantal definities en beweringen is aangegeven dat ze fout zijn, maar niet bij allen.
   • Je moet dus zelf een foute bewering zoeken en verbeteren.
   • Als je overtuigd bent dat alles op die pagina correct is, hoef je natuurlijk geen fouten meer te verbeteren. In dit geval neem je in je uitwerking een verklaring op dat er geen fouten meer staan.
   • Je mag de pagina niet mer uitbreiden met nieuwe definities en beweringen en zeker niet eerst een fout injecteren om deze dan te verbeteren.
3. Maak samen met je groepsgenoten een eerste specificatie van het artefact in het werkstuk.
   • Maak daartoe ook het nodige domeinmodel.
   • Geef de specificatie op drie manieren weer, zo als hieronder aangegeven.
4. Kies één onderdeel van jullie artefact.
   • Verzeker je ervan dat elk groepslid een ander onderdeel heeft gekozen.
   • Breid het domeinmodel uit met de "interne" fenomenen die nodig zijn om dit onderdeel te kunnen specificeren.
   • Geef op dezelfde drie manieren de specificatie van je onderdeel.
   • Het is op dit moment nog niet nodig dat alle onderdelen gespecificeerd zijn en dat ze precies bij elkaar passen, maar het moet wel een serieuze eerste aanzet zijn.
5. Denk, als je alles op de werkstukpagina in context ziet, nog eens na over hulpdefinities die het verhaal eenvoudiger kunnen maken. Je kunt je laten inspireren door de definities van de oefenpagina.

Product

1. Zolang nog fouten op Beweren en bewijzen/het verhaal/4. De taal/oefenpagina staan: 1 verbeterde definitie of bewering op de pagina zelf.
2. In de uitwerking van deze taak: de definitie of bewering vóór en na je verbetering. Indien je overtuigd bent dat niets meer te verbeteren valt, een korte verklaring.
3. Op de werkstukpagina:
   1. het domeinmodel,
   2. de specificatie van het hele artefact voor zover de groep het erover eens is,
   3. de specificatie van één onderdeel.
4. Deze specificaties in drievoud:
   1. In heldere natuurlijke taal, zo elegant en duidelijk mogelijk.
   2. Als door Coq goedgekeurde formule, leesbaar opgemaakt conform de richtlijnen.
   3. Een letterlijke terugvertaling van deze formule naar natuurlijke taal.
5. In de uitwerking van deze taak:
   1. een doorklikmogelijkheid naar de werkstukpagina,
   2. de naam van je onderdeel,
   3. indien het de groep nog niet eens kon worden over de specificatie van het geheel: je eigen versie van deze specificatie.

Reflectie

• Kloppen de bereiken van je kwantoren? Staan er voldoende haakjes?
• Is het leesbaar opgemaakt en niet te breed voor de beamer?
• Zijn de specificaties systematisch afgeleid?
• Kun je het e.e.a. leesbaarder maken door hulpdefinities?
• Op het tentamen moet je op niveau van Beweren en bewijzen/het verhaal/4. De taal/oefenpagina beweringen kunnen opstellen en fouten verbeteren. Kun je dat nu?

Inleveren

• Je uitwerking maak je hier.
• Zet op de eerste regel van je uitwerking precies dit:

  {{individuele opdracht}}

• Uiterste inleverdatum: {{{deadline}}} en geen minuut later -
• Wil je deelnemen aan het responsiecollege moet je uitwerking op tijd af zijn en (indien MediaWiki correct functioneert) in het goede lijstje hieronder verschijnen.

---

"{{{deadline}}}" contains an extrinsic dash or other characters that are invalid for a date interpretation.

"{{{deadline}}}" contains an extrinsic dash or other characters that are invalid for a date interpretation.