Eigenschap:Specgeheelcommentaar

Dit is een eigenschap van type Tekst.

Pagina's die de eigenschap "Specgeheelcommentaar" gebruiken

Er zijn 236 pagina's die deze eigenschappen gebruiken.

(vorige 500 | volgende 500) (20 | 50 | 100 | 250 | 500) bekijken.

B
Beweren en bewijzen/2011-12/feedback/ATB-deel1 +	„de trein is nog niet begonnen met afremmen na drie seconden” is moeilijk te formaliseren; beter is zoiets als: „als de trein al de afgelopen drie seconden te snel heeft gereden, dan ...” „de trein staat niet stil” is triviaal waar als de trein te snel rijdt. Formule ontbreekt, maar was niet absoluut vereist.  +
Beweren en bewijzen/2011-12/feedback/ATB-deel1-her +	De specificatie is erg complex; is het niet voldoende om te zeggen dat de trein tot stilstand komt, misschien binnen een bepaalde afstand? Na de regel <tt>RT u</tt> ontbreekt kennelijk een logische operator.  +
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel1 +	Er gaan hier veel dingen mis: * Er is geen specificatie in natuurlijke taal. * Er zit minimaal 1 syntaxfout in de formule. * Er worden allerlei interne fenomenen gebruikt. * Ik denk dat jullie bij de externe aannames willen zeggen dat er de hele periode van 30 seconden zowel stroom is als weinig licht. Want als ik Harm goed heb begrepen, moet jullie lamp uitgaan als na 18 seconden de zon opkomt. * Splits de specificatie in natuurlijke taal in kleine begrijpelijke zinnen die je dan uiteindelijk in de formule koppelt via en-tekens.  +
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel1-her +	Ook hier staan haakjes op rare plaatsen, maar dan niet alleen typografisch, maar ook qua inhoud. Verder is het eigenlijk natuurlijk niet genoeg om te eisen dat er op een bepaald moment te weinig licht is. Het was immers de bedoeling dat de lamp na 17 sec uit kon gaan als er dan opeens wel licht genoeg was?  +
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel2 +	Al ziet hij er wel een beetje verdacht uit.  +
Beweren en bewijzen/2011-12/feedback/Beertender-deel1 +	In de formule wordt „perfectBiertje” gebruikt, een predicaat dat je niet hebt gedefiniëerd. Misschien bedoel je „perfectBier”? „gedurende 10” – 10 wat? 10 aardappels? Ik kan niet de hele nederlandse tekst lezen. Het idee heb je wel goed begrepen, inhoudelijk klopt de formule en wat ik kan lezen van de tekst.  +
Beweren en bewijzen/2011-12/feedback/Blokfluit-deel1 +	ontbreekt  +
Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel1 +	In de natuurlijke-taal-tekst spreek je over „een signaal naar het alarm en naar de sprinkler”, dat is een intern signaal van het systeem en hoort niet in een specificatie thuis van dingen die aan de buitenkant gebeuren.  +
Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel2 +	Er worden twee verschillende specificaties gegeven. De eerste is niet te bewijzen (en eindigt met ; i.p.v. .), in de tweede staat weer een all-kwantor met /\ i.p.v. –>.  +
Beweren en bewijzen/2011-12/feedback/PA-systeem-deel1 +	idem dito  +
Beweren en bewijzen/2011-12/feedback/Printer-deel1 +	De samenhang van invoer en resultaat is niet gespecificeerd.  +
Beweren en bewijzen/2011-12/feedback/Rekenmachine-deel2 +	Klopt, de machine kan meer. Maar deze specificatie is interessant omdat bewezen wordt dat iets heel algemeens, krachtigs ook voor een specifiek, eenvoudig doel geschikt is.  +
Beweren en bewijzen/2011-12/feedback/Roltrap-deel1 +	De formule bevat een syntaxfout na „d<200”. Op zich een prima stelling; zou je hem nog een beetje interessanter kunnen maken door te stellen dat de passagier helemaal naar boven gebracht wordt, dus dat de roltrap aan blijft staan tot hij boven is?  +
Beweren en bewijzen/2011-12/feedback/Roltrap-deel2 +	Hier ook weer: Jullie schrijven de specificatie zó op dat alleen relevant is of iemand op het tijdstip dat de roltrap start de noodknop indrukt. Daarna de noodknop indrukken heeft geen gevolgen meer erop of de persoon boven aankomt of niet.  +
Beweren en bewijzen/2011-12/feedback/Segway-deel1 +	Het belangrijkste ontbreekt  +
Beweren en bewijzen/2011-12/feedback/Segway-deel2 +	Het is geen onzinnige specificatie, maar ze gaat voorbij aan de meest essentiële eigenschap van de Segway: dat je je ermee kunt verplaatsen en dat het niet omvalt.  +
Beweren en bewijzen/2011-12/feedback/Vaatwasser-deel1 +	In orde.  +
Beweren en bewijzen/2011-12/feedback/Vaatwasser-deel2 +	In <tt>(forall td:T, td >= ts /\ td < ts + 10800 /\ deur_dicht td)</tt> zou een implicatie moeten staan; datzelfde geldt ook voor de timer.  +
Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel1 +	ontbreekt  +
Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel2-her +	Omdat deze specificatie de inconsistente aanname <tt>forall j:C, c=j /\ IT t (dr j)</tt> bevat, kun je hiermee eigenlijk alles bewijzen, zelfs zonder de rest van het verwarmingssysteem. Ik vermoed dat je bewijs daarom werkt.  +
Beweren en bewijzen/2011-12/feedback/airco-deel1 +	Door het algoritme dat in de formule wordt gebruikt is het wat lastig te zien of de formule goed past bij de natuurlijke taal, maar ik geloof dat het wel klopt.  +
Beweren en bewijzen/2011-12/feedback/airco-deel2 +	Ook hier weer 'de airco gaat aan' terwijl dat niet in de formule staat. En waar blijft de 'als de airco aanstaat dan zuigt hij buitenlucht aan'? Dat 'buitenlucht aanzuigen' staat voor de eerste pijl en kan ik dus niet met een 'dan' situatie rijmen.  +
Beweren en bewijzen/2011-12/feedback/airco-deel2-her +	Wat betekent 'er is lucht aangezogen in 1 seconde' precies? Is hij dan een interval bezig? Of alleen op precies 1 seconde na het eerste moment? Jammer dat jullie het verschil tussen kleiner en groter niet weten: t is niet groter of gelijk aan t+10! De uitleg over dat 't+1' eigenlijk een interval is, snap ik denk ik wel, maar het staat er een beetje knullig.  +
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel1 +	Bij de specificatie van het geheel horen eigenlijk alleen externe fenomenen te worden gebruikt. Ik weet niet precies hoe dat in jullie syntax past als formule, maar ik zou zoiets verwachten als: 'Voor elke sleutel geldt dat als het profiel van die sleutel past bij het slot, dan is (kan/gaat?) het slot open. En als het slot_open is, dan moet er een sleutel zijn met een passend profiel.' De onderdelen moeten dan ingewikkeld naar de hoogtes van de pinnen gaan kijken om te zorgen dat het slot ook echt open gaat (of juist niet).  +
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel1-her +	Volgens mij staat hier weer een ∃ gekoppeld aan een → wat dus zelden iets zinnigs oplevert. Verder gebruiken jullie hier sleutelInSlot die nergens in de onderdelen nodig is, dus kan hij hier ook wel weg. En omdat jullie al meteen die ∀ u, c en k meegeven (nu met goede haakjes), heeft onderdeel Cylinder ook meteen wat hij nodig heeft en is onderdeel Profiel dus eigenlijk ook niet nodig.  +
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel2 +	Ik begrijp niet zo heel goed wat nu het verschil is tussen 'profielMatch' en 'juisteSleutelpinHoogte'. Is dat nu wezenlijk iets anders? Of eigenlijk hetzelfde. Ik heb sleutels die wel in het slot passen, maar die niet kunnen draaien. Betekent dat dan dat 'profielMatch' wel waar is, maar die 'juisteSleutelpinHoogte' niet? Verder lijkt het hier alsof die aanname over 'juisteSleutelpinHoogte' precies dezelfde is als bij het onderdeel SleutelPinnen. Ondanks dat er dan een ∀ u staat in de specificatie, maakt dat het bewijs niet moeilijker.  +
Beweren en bewijzen/2011-12/feedback/elektrische tandenborstel-deel1 +	Waarom hier nog een definitie van voldoende_stroom? Dit is typisch een plek (misschien ook bij de Controller trouwens) waar hulppredikaten wel zin hebben. Door de complexe vorm is moeilijk te begrijpen wat de verschillende 'cases' nu eigenlijk zijn. Door hulppredikaten te maken voor iets als 'is precies 2 minuten aan' is makkelijker te controleren dat de formule bij de natuurlijke taal past.  +
Beweren en bewijzen/2011-12/feedback/elektrische tandenborstel-deel2 +	Wel een beetje jammer dat hier als voorwaarde al voldoende_stroom is meegegeven. Nu is het helemaal niet van belang wat de definitie van voldoende_stroom is. Als je hem in het script vervangt door t<>t werkt het bewijs nog steeds. Wel positief is dat jullie desda's hebben gebruikt. Vaak zijn de niet-bewijzen lastiger.  +
Beweren en bewijzen/2011-12/feedback/fiets-deel1 +	De specificatie van het geheel is geen beschrijving van wat de onderdelen als de kettingkast allemaal doen, maar juist wat je aan de buitenkant ziet. Dus iets als 'indien er met kracht n op tijdstip t op de trappers wordt getrapt en de dynamo staat dan op het voorwiel en het stuur staat in richting r, dan rijdt de fiets met snelheid F(n) op tijdstip t in richting r en geeft de lamp G(n) lumen licht'. Hierbij zijn F en G abstracte functies die bij jullie misschien te maken zijn als opeenstapeling van de functies KO, OO1, OO2, OS et cetera. In het bijzonder gaat er ook iets mis met de syntax. Zo staan er twee mogelijke formules gegeven.  +
Beweren en bewijzen/2011-12/feedback/fiets-deel1-her +	Er staan vier &exists; in die allemaal fout zijn. Als je deze definitie in Coq bekijkt, zie je ook dat Coq ook niet goed weet wat hij met s en r aanmoet, want die komen verder niet meer voor. En de eerste twee &exists; zorgen voor een standaardfout.  +
Beweren en bewijzen/2011-12/feedback/fiets-deel2 +	Het was beter geweest als jullie hier niet de abstracte samenstelling van functies hadden gebruikt, maar de concrete invulling. Dan hadden jullie echt moeten laten zien dat je er mee kon rekenen.  +
Beweren en bewijzen/2011-12/feedback/flitspaal-deel1 +	Er staat niets.  +
Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel1 +	Waar komt die ~bezig vandaan in de formule? Door de keuze van jullie kwantoren hebben jullie een standaardfout geintroduceerd. En is het redelijk om alleen maar te eisen dat er stroom is aan het begin van een cyclus? Of moet het er continu zijn gedurende die x+10 seconden? Overigens zie ik hier weer niets terugkomen over dat al dan niet nodzakelijke koelen. Is dat dan toch niet van belang? En waar komt die 10 vandaan? In de onderdelen zie ik zo snel alleen maar een 3 en een 5 staan, dus wordt het dan lastig om te bewijzen dat er na 10 seconden iets klaar is.  +
Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel1-her +	Het ziet er op zich niet onredelijk uit, maar ik heb toch wel mijn twijfels of dit te bewijzen valt uit deze onderdelen. Succes!  +
Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel2 +	Behalve wat rare haakjes bij 'gg (t) f' staat er niets fout in deze eigenschap. Echter, aangezien de aannames verdacht veel lijken op wat de onderdelen nodig hebben, verwacht ik een zeer simpel bewijs.  +
Beweren en bewijzen/2011-12/feedback/frituurpan-deel1 +	Afgezien van wat tikfouten ziet dit er heel werkbaar uit. Er gaat nog iets mis met Snack_klaar. Daar wordt nu weer een boolean ingevuld terwijl er een of andere temperatuur van minstens 75 graden bedoeld wordt. Verder hebben jullie een hulpdefinitie Programma_correct gemaakt, die je hier had kunnen gebruiken, maar dat doen jullie toch niet.  +
Beweren en bewijzen/2011-12/feedback/frituurpan-deel2 +	Ook hier min of meer dezelfde fouten. Voor de eerste pijl staat dat als voor alle c geldt dat c groter gelijk 75 is, dan... Maar dat geldt natuurlijk niet voor alle c:C. Bijvoorbeeld niet voor c is 5. En aan het eind dezelfde fout als bij onderdeel mand. Verder is het raar dat jullie bij focus nog schrijven dat er een beveiligingssysteem moet zijn dat de boel niet oververhit kan raken, maar daar zeggen jullie niets over in de specificatie van het geheel.  +
Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel1 +	Het 'onvoldoende' staat hier vooral doordat je interne onderdelen noemt. Het gaat er hier juist om dat je alleen externe dingen noemt. En dus heb je misschien wel een extren fenomeen 'erLigtprijs: P->X->Y->Z->B' nodig om te kunnen checken dat als je de grijphaak naar een positie brengt waar een prijs ligt, je dan ook een prijs krijgt. Misschien is het hier overigens wel verstandig om een automaat te maken zoals ik ze ken: je geeft eerst aan hoe lang je vooruit gaat, dan hoelang naar links en meer kun je niet kiezen. Op zo'n manier kun je aan een tijdsinterval van 6 seconden vooruit precies een afstand van 6x10 posities naar voren. Als je tussendoor terug kunt, is het heel lastig aan te geven waar je bent na een bepaalde tijd.  +
Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel1-her +	Ook hier staan de kwantoren opvallend vooraan, waar dat misschien niet handig is. Verder mis ik een ∀p en enkele sluithaken.  +
Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel2-her +	Ziet er op zich goed uit. Echter, je gebruik van de hypothesis doet vermoeden dat het toch echt niet klopt.  +
Beweren en bewijzen/2011-12/feedback/kassa-deel1 +	Oei, hier staan wel erg vage 'ongeveers' in terwijl er in de formule exacte getallen staan. Dat kan niet bij elkaar passen. Zorg er ook voor dat het volkomen evident is dat die 8.1 in de tekst te maken heeft met die 10.3 in de formule. Verder gaat het hier geloof ik ook weer mis met de koppeling tussen kwantoren en voegtekens. Zou je hier misschien kunnen bewijzen dat als op tijdstip t1 artikel s1 is aangeboden, op tijd t2 artikel s2 (waarbij t2 > t1) en op tijd t3 de knop 'scannen voltooid' is ingedrukt (t3>t2), dat dan op t3+x op het scherm de totaalprijs van s1+s2 staat en op t3+y er een bonnetje is met die prijs?  +
Beweren en bewijzen/2011-12/feedback/kassa-deel1-her +	Ook hier geldt dat de specificatie in natuurlijke taal niet te lezen is. Geef de werking weer door korte zinnen zonder variabelen. Zodat duidelijk wordt waar het ongeveer over gaat. Geef vervolgens de formule en jullie huidige zinnen (nou ja, liever iets leesbaarder) om te zien dat de formule bij de natuurlijke taal past. Verder zitten er technisch wel wat rare constructies in. Rond de tweede pijl staat een consructie die neerkomt op '∀ r, A → B r' waarmee ik bedoel dat er voor de pijl een eis staat die onafhankelijk van r is, maar na de pijl een conclusie die wel waar is voor alle r. Volgens mij betekent dit dat hier een willekeurig totaalbedrag kan worden ingevuld. Zou het helpen om die ∀ r van voor de pijl te veranderen in een ∃ r na de pijl? Je weet dan in de spec van het geheel niet precies welke r dat is, maar in principe is dat het opgetelde bedrag van alle gescande artikelen en bijbehorende prijzen. (Dat lijkt me overigens moeilijk te bewijzen als er niet expliciet gezegd wordt welke artikelen gescand zijn.) En even later staat bij de pinpassen een ∀ x. In jullie Coq-script zetten jullie hier haakjes omheen en dat lijkt me verstandig. Maar volgens mij eisen jullie nu dat er 6 seconden lang continu een pinpas wordt aangeboden. Is dat wel de bedoeling? Is het niet voldoende om te zeggen dat als er een moment binnen die 6 sec is waarop er een pinpas is aangeboden, dan is het in orde? En is die ∀ pc hier ook wel goed?  +
Beweren en bewijzen/2011-12/feedback/kassa-deel2 +	Sowieso jammer dat de specificatie van het geheel een stuk simpeler is geworden dan dat hij was. Wat verder jammer is, is dat jullie 'er is een moment dat de pinpas wordt aangeboden' qua interval precies overeenkomt met wat het onderdeel nodig heeft. Hierdoor wordt het bewijs een stuk simpeler.  +
Beweren en bewijzen/2011-12/feedback/koelkast-deel1 +	Ziet er goed uit.  +
Beweren en bewijzen/2011-12/feedback/koelkast-deel1-her +	Door de layout is de helft van de tekst niet te lezen. Waarom is die i2 ingevoerd? Kan dat niet gewoon met i? Verder lijkt er een 'er is een' gekoppeld te zijn aan een implicatie, wat altijd bijzonder verdacht is.  +
Beweren en bewijzen/2011-12/feedback/lift-deel1-her +	Hier komen opeens weer een heleboel nieuwe hulpdefinities. Waarom stonden die niet in de daarvoor bedoelde sectie 'hulpdefinities'. In het bijzonder mist de natuurlijke taal bij deze nieuwe definities, waardoor het lastig is te zien of hier nu iets goeds staat of niet. Wat betekent Omhoog hier opeens? Is dat een nieuw predikaat?  +
Beweren en bewijzen/2011-12/feedback/lift-deel2-her +	Zoals bij het netwerk al opgemerkt: dit kan eigenlijk niets worden. De specificatie van het geheel kijkt als blackbox naar het systeem en kent dus alleen de externe fenomenen. Maar jullie eigenschappen praten allemaal over interne fenomenen. Verder zijn definities als WachtlijstMoetLeegZijn zonder toelichting echt niet te lezen.  +
Beweren en bewijzen/2011-12/feedback/loopband-deel1 +	Hier wordt weer een nieuw predikaat AanknopIngeschakeld gebruikt. Verder is de natuurlijke taal veel vager dan de formule. Daar staat dat de snelheid naar 0 gaat, maar niet wanneer. Terwijl in de formule staat dat dat over 1 seconde is. (Het lijkt me dat dit niet te bewijzen is met jullie huidige onderdelen, zie commentaar Band.) Maak ook het onderscheid tussen t en T, v en V en a en A.  +
Beweren en bewijzen/2011-12/feedback/loopband-deel2 +	Jammer dat er geen intervallen gebruikt worden, maar er alleen 1 seconde vooruit gekeken wordt. Ook jammer dat de interessante specificaties als 'KnoppenIngedrukt' met allerlei exists erin blijkbaar niet van belang zijn.  +
Beweren en bewijzen/2011-12/feedback/luchtontvochtiger-deel1 +	Bij de specificatie van het geheel gaat het er om dat je van buiten kijkt en zegt wat je zou willen bij dit artefact. In het bijzonder moet je hier dus geen onderdelen noemen, maar alleen externe fenomenen. Hierin maak je overigens hetzelfde soort fouten als in de CPU.  +
Beweren en bewijzen/2011-12/feedback/luchtontvochtiger-deel1-her +	Zelfde soort fouten in de formule als bij de onderdelen. En in de natuurlijke taal staat iets geks als 'dan is er vochtige lucht in', terwijl ik denk dat dat meer een 'als' stuk is.  +
Beweren en bewijzen/2011-12/feedback/magnetron-deel1 +	Eigenlijk zou je hier niet alleen moeten eisen dat de deur aan het begin dicht is, maar dat hij dat de hele duratie d blijft.  +
Beweren en bewijzen/2011-12/feedback/magnetron-deel2 +	Deze is in elk geval beter opgeschreven door pas kwantoren te introduceren als ze nodig zijn, wat bij de onderdelen vaak niet het geval is. Het is een beetje jammer dat de intervallen waarop aannames gelden en de eindtemperatuur zo'n beetje letterlijk hetzelfde zijn in de spec van het geheel en de onderdelen. Daardoor krijgen jullie nauwelijks de kans om jullie vaardigheden met het rekenen met getallen te tonen.  +
Beweren en bewijzen/2011-12/feedback/ov-oplader-deel1 +	Ook hier is de koppeling tussen formule en natuurlijke taal niet goed. Verder vind ik het een beetje een rare specificatie. Als ik op moment t de OVchip in de lezer heb en er allerlei andere dingen gebeuren precies op t+3 en t+9 en ik mijn kaart op t+5 weer uit de lezer haal, lijkt het me sterk dat ik op t+10 een verhoogd saldo heb op die kaart. Ik zou verwachten dat je in elk geval eist dat die kaart de hele 10 seconden in die lezer blijft zitten. (Ook al hebben je onderdelen het misschien alleen maar echt nodig op tijdstip t en t+10.) Verder heeft Robin in zijn commentaar gelijk dat hij niet weet wanneer de gebruiker precies de pincode heeft ingevoerd en wanneer zijn pinpas. Maar je kunt misschien wel limieten stellen. Jullie automaat doet het alleen als de pinpas tussen 0 en 3 seconden na het insteken van de ov-chipkaart er in zit (en blijft zitten totdat de pincode is gecheckt) en vervolgens binnen 0 en 6 seconden de (goede) pincode heeft ingetoetst, dat dan het saldo is bijgeschreven ergens tussen 0 en 9 seconden.  +
Beweren en bewijzen/2011-12/feedback/ov-oplader-deel2 +	Jullie gebruiken dezelfde onduidelijke constructie voor 'als er binnen twaalf seconden' als bij de onderdelen, dus hoewel niet helemaal helder, zal het wel bij elkaar passen. Wel jammer dat jullie zondigen tegen de syntax van onze grammatica, precies op dat punt waar Coq minder strikt is dan wij. Jullie zetten namelijk geen haakjes op plekken waar kwantoren gekoppeld worden aan logische voegtekens.  +
Beweren en bewijzen/2011-12/feedback/stortbak-deel1 +	Hier wordt een kans gemist. De specificatie van het geheel praat over dingen die de gebruiker niet interesseren, bijvoorbeeld hoe vol de bak is. De gebruiker wil alleen weten dat niet meer water dan nodig verbruikt wordt en dat hij kan doortrekken vanaf een bepaald moment na het vorige doortrekken.  +
Beweren en bewijzen/2011-12/feedback/wasdroger-deel1 +	idem dito  +
Beweren en bewijzen/2011-12/feedback/waterkoker-deel1 +	Technisch gesproken klopt het wel wat er staat. Maar het ziet er wel raar uit: alleen maar zeggen wanneer het lampje niet brandt. Ik zou hier verwachten dat je ook wil aangeven wanneer het wel aan is. Verder geldt de opmerking over intervallen en een vreemde t+120 hier natuurlijk ook.  +
Beweren en bewijzen/2011-12/feedback/waterkoker-deel2-her +	Oh, ik zie het al: jullie proberen niets meer te bewijzen over het niet branden van het lampje. In de tweede eigenschap is het een beetje overbodig om voor alle c te zeggen en dan c te beperken tot 100. Dan had je toch ook gewoon iets als "water t 100" kunnen zeggen? Nu schrijf je iets simpels vrij ingewikkeld op. Het ziet er een beetje flauw uit.  +
Beweren en bewijzen/2011-12/feedback/windmolen-deel1 +	Dikke logische fout met existentiële kwantor.  +
Beweren en bewijzen/2011-12/feedback/windmolen-deel2 +	Staan er in de specificatie van het geheel niet details van binnen de molen waarin de gebruiker niet geïnteresseerd is? Als er koren en wind is en alles goed afgesteld, krijgt men meel. So staat het er ook in natuurlijke taal. Maar in de formule duiken allerlei assen en kruisen op. Kan dit niet eenvoudiger?  +
Beweren en bewijzen/2011-12/feedback/xbox360-deel1 +	Alles lijkt op hetzelfde moment te gebeuren, dus dan heb je die tijd niet nodig. Ook ziet die 'er is wel of geen druk op de controller' er heel raar uit. En er lijkt niet echt een koppeling te zijn tussen wat de gebruiker nu doet en wat er als resultaat te zien is.  +
Beweren en bewijzen/2012-13/feedback/Alarmsysteem-deel1 +	Via de hulpdefinitie „alarmUitgeschakeld” staat er een intern signaal in de specificatie van het geheel.  +
Beweren en bewijzen/2012-13/feedback/Bankkluis-deel1 +	Ook hier weer een syntaxprobleem.  +
Beweren en bewijzen/2012-13/feedback/Bankkluis-deel2-her +	Tja, hier zit natuurlijk precies diezelfde vreemde plaatsing van de ∀ t2, dus waarschijnlijk kun je de stelling wel makkelijk bewijzen. Als jullie nu in de spec van het geheel er voor gekozen hadden te zeggen dat de sleutel binnen 7 minuten is ingestoken dan had de stelling toch ook moeten kloppen? Want jullie onderdelen zijn tevreden als je het binnen 10 minuten doet, dus als je als aanname geeft dat het binnen 7 minuten gebeurt, moet dat toch ook goed gaan? In dat geval hadden de intervallen niet precies gepast en hadden jullie kunnen laten zien dat jullie ook kunnen werken met intervallen. Echter: ik heb dat geprobeerd en dan moet ik uit 't3 in (t5, t5 + 10]' bewijzen dat ook 't3 in (t5, t5 + 7]'. Maar dat kan natuurlijk niet, want t3 zou best t5+ 9 kunnen zijn! Dit testje onderstreept volgens mij de incorrectheid van jullie specificaties.  +
Beweren en bewijzen/2012-13/feedback/Draaideur-deel1 +	Ook hier weer en/of-fouten. En ook weer veel ontbrekende tijdsparameters. Als ik jullie specificatie van het geheel zie, hebben jullie met de draaideur een ander idee dan ik had. Het lijkt jullie niet te gaan om objecten van de ene kant van de deur naar de andere te brengen, maar puur te kijken wanneer de deur automatisch draait of niet.  +
Beweren en bewijzen/2012-13/feedback/Draaideur-deel2 +	Maar slechts met hulp van mij.  +
Beweren en bewijzen/2012-13/feedback/Dubbele schuifdeur-deel1 +	De specificatie is formeel correct en zegt ook iets zinvols, maar je schreef aan het begin dat één van de belangrijkste eisen was dat personen naar binnen of naar buiten kunnen. Daarvoor is het vereist dat beide deuren kort na elkaar opengaan.  +
Beweren en bewijzen/2012-13/feedback/Dubbele schuifdeur-deel2-her +	De tijdsduur van het naar-binnen-gaan is in de formule aangepast, maar helaas niet in de informele specificatie.  +
Beweren en bewijzen/2012-13/feedback/Eukaryoot-deel1 +	In de natuurlijke taal staat alleen maar iets over 'aanwezig zijn' helemaal niet dat dat soms op tijd t en soms op tijd t+3 is. Dat kan dus niet kloppen. Verder staat het ook wel raar dat die dna precies op t+3 aanwezig moet zijn. Misschien kun je gebruiken dat als iets aanwezig is op tijdstip t en er niets kan reageren, dat dan alles aanwezig blijft op tijdstip t+1?  +
Beweren en bewijzen/2012-13/feedback/Eukaryoot-deel2 +	De plaatsing van de kwantoren is wel raar. Die t is bijna nergens nodig, maar staat wel helemaal vooraan. Verder is het wel een sterke eis dat al die stoffen altijd aanwezig zijn. Is het voor een van de onderdelen van belang dat de stoffen ook in het verleden (voor t) aanwezig waren?  +
Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel1 +	Het is heel raar dat jullie klant zelf tot 4 moet tellen. Want als hij te vroeg of te laat drukt, krijgt hij geen bon. Dat moet dus echt anders. Je zou hier ook weer kunnen splitsen naar korte zinnen: - Als de klant op stop drukt, dan komt er 2 sec later een bon met het huidige saldo. (Misschien eisen dat het huidige slado > 0 is.) - Als de klant een goede fles invoert, is het huidige saldo op het scherm 2 sec later verhoogd met het bedrag dat hoort bij het type fles. - Als de klant een goed krat invoert, is het .... - Als de klant een foute fles invoert, staat 2 sec later het huidige saldo op het scherm, plus een foutmelding - Etcetera.  +
Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel1-her +	De specificatie in natuurlijke taal ontbreekt, dus dit kan niet goed zijn. Zelfs niet voldoende. Tevens zondigen jullie tegen het intern/extern principe. In de spec van het geheel staan normaal gesproken alleen maar externe fenomenen, maar ik zie bij jullie ook dingen als 'goedO' en 'bandSignaal' staan. Zonder op details te letten verwacht ik hier zinnen als: 'Als er een goedgekeurd object is ingevoerd en er staat een bepaalde saldoinformatie op het scherm dan staat zoveel tijd later de met de juiste waarde toegenomen saldoinformatie op het scherm' en 'Als er een afgekeurdobject is ingevoerd verandert de saldoinformatie niet, maar komt er wel een foutmelding op het scherm'. Zeggen jullie hier nu dat 'objectInvoer t o' altijd waar is? Of wat betekent die /\ daar vooraan?  +
Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel2 +	Het blijft vreemd dat het in jullie systeem blijkbaar nodig is om te eisen dat er de vorige seconde niets of niets goedgekeurds is ingevuld. Verder hebben jullie hierbij de \/ en /\ op hetzelfde niveau geplaatst, terwijl de /\ dieper zou moeten zitten.  +
Beweren en bewijzen/2012-13/feedback/Frisdrankautomaat-deel1 +	Dit is wel een beetje een raar systeem. Je vraagt een leverancier als het ware een ding te maken dat goed werkt als er precies een euro in wordt gegooid. En als de klant precies 2 sec wacht met selecteren. Ik denk dat jullie bedoelen: als er op tijdstip t1 g geld is ingeworpen en op een mogelijk later tijdstip t2 een selectie s is gemaakt en de prijs van s is lager dan g, dan is er een aantal seconden later frisdrank behorend bij selectie s in de bak en ligt er wisselgeld van (g - prijs s) in het wisselgeldbakje. Maar misschien willen jullie wel iets anders...  +
Beweren en bewijzen/2012-13/feedback/Frisdrankautomaat-deel2 +	Behalve dan de layout van de formule.  +
Beweren en bewijzen/2012-13/feedback/Halon-systeem-deel1 +	Ook hier missen soms tijdsparameters. En wat betekent die ; midden in de formule? En weten jullie zeker dat de pijl van rechts naar links ook geldt?  +
Beweren en bewijzen/2012-13/feedback/Koelkast-deel1 +	Technisch gesproken niet slecht, maar wel heel flauw omdat de onderdelen tamelijk flauw zijn.  +
Beweren en bewijzen/2012-13/feedback/Koelkast-deel1-her +	Ziet er op zich goed uit, maar ik ben niet zeker dat je hem kunt bewijzen. (Er van uitgaande dat je dat met die 'aan' oplost natuurlijk, want anders weet ik wel dat je het niet kunt bewijzen.)  +
Beweren en bewijzen/2012-13/feedback/Koelkast-deel2 +	Ook hier een (zelfde) syntaxfout in de formule. Verder staat het een beetje raar dat je als voorwaarde voor het branden van het deurlampje moet hebben dat hij eerst 30sec open moet zijn om dan 1 msec later het lampje aan te hebben. Ook hier komt de gesuggereerde structuur niet overeen met de echte structuur van de formule!  +
Beweren en bewijzen/2012-13/feedback/Koffiezetapparaat-deel1 +	Syntax ∀ of A? Ziet er op zich goed uit, maar ook hier weer de vraag of een verzameling knoppen en een functie die aan een knop een drank koppelt niet handiger zou zijn? Dan zou je iets kunnen zeggen als 'voor alle knoppen k geldt, als er op tijdstip t op knop k wordt gedrukt dan stroomt er 1 seconde later gedurende 3 seconden (drank k) uit de machine'. Maar misschien willen jullie juist wel onderscheid gaan maken tussen de duur van de verschillende dranken: bij het apparaat bij ons op de afdeling komt de chocomel er 'direct' uit terwijl de koffie een halve minuut duurt omdat die nog door een filter geperst moet worden of zo. Door de verschillende dranken echt verschillende trajecten te laten volgen kun je het spannender maken.  +
Beweren en bewijzen/2012-13/feedback/Koffiezetapparaat-deel2 +	Jullie gebruiken 'totaal' als een extern fenomeen, maar volgens het netwerk is het alleen maar intern beschikbaar. Ook hier ontbreken haakjes en is de opmaak niet conform de kwaliteitscriteria. En wat is het doel van die ∀ d:D? Er wordt helemaal geen d gebruikt in de formule! Dit zorgt er ook voor dat je straks in het bewijs een rare D tegenkomt.  +
Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel1 +	i.p.v. =:. De haakjes om formules zijn overbodig omdat de prioriteiten al goed werken.  +
Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel2 +	Hetzelfde probleem als bij de bedrijfsurenteller: Als de stofzak twee uur lang niet geleegd wordt, dan wordt hij geleegd.  +
Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel2-her +	is nu correct.  +
Beweren en bewijzen/2012-13/feedback/Lift-deel1 +	Ik snap dat een formele specificatie met tijd nu misschien nog te moeilijk is, maar in de natuurlijke taal had er toch echt wel iets kunnen staan wanneer dat object dan verplaatst is en wanneer de deuren open zijn. Dat kan heel expliciet ,et jullie 'transportTijd' of impliciet met iets als 'er is daarna een moment waarop'.  +
Beweren en bewijzen/2012-13/feedback/Lift-deel1-her +	Jullie specificatie van het geheel is volgens mij niet bewijsbaar uit de onderdelen. Om te beginnen zie ik de vertraging van 1 sec van het bedieningsPaneel niet terug. Verder is de koppeling over de plek waar de lift is bij het begin van het verhaal niet goed. Zie boven.  +
Beweren en bewijzen/2012-13/feedback/Lift-deel2 +	Die van het hele systeem ziet er wel goed uit, maar die van het TransportMechanisme zelf is toch wel raar.  +
Beweren en bewijzen/2012-13/feedback/Magnetron-deel1 +	Er staat geen uitleg wat dit in natuurlijke taal betekent. En in de formule staat een 'MagnetronActief' die nergens is uitgelegd. Zonder een goede specificatie van het geheel in natuurlijke taal kan er weinig gemaakt worden van het werkstuk.  +
Beweren en bewijzen/2012-13/feedback/Magnetron-deel1-her +	Deze spec is niet heel slecht, maar net niet goed genoeg om in elk geval iets serieus te kunnen bewijzen. In het bijzonder hebben jullie hier nu geloof ik zo'n enge combinatie van &exists; en → gebruikt... Het type van object_opgewarmd is verkeerd.  +
Beweren en bewijzen/2012-13/feedback/Magnetron-deel2-her +	Maar omdat deze spec nagenoeg gelijk is aan een deel van de spec van de draaiplaat, zal het bewijs tamelijk simpel zijn.  +
Beweren en bewijzen/2012-13/feedback/Melkrobot-deel1 +	Dit is nog niet goed, maar ziet er niet slecht uit. In elk geval wordt er uitgesproken wat de bedoeling is. Technisch gaat er nog wel wat mis. Zo bestaat koe k na de → niet meer wegens de haakjes bij de ∃ k. En 'Melk v' stond ook niet in het domeinmodel. Ik vermoed dat je het beste kunt beginnen met ∀ t in T, ∀ k in K, koeID k t ->'  +
Beweren en bewijzen/2012-13/feedback/Melkrobot-deel1-her +	Davids toevoeging in natuurlijke taal in de formule is niet verwerkt. Er wordt een predikaat Melk gebruikt dat niet is gedefinieerd. Op zich hebben jullie bijna een niet triviale maar wel bewijsbare stelling opgeschreven. Er hoeven slechts kleine dingen in de onderdelen te worden verbeterd.  +
Beweren en bewijzen/2012-13/feedback/Melkrobot-deel2 +	Maar ook hier kan de opmaak van de formule wel beter. Verder hebben jullie duidelijke hulp gehad bij het opstellen van deze specificatie van het geheel.  +
Beweren en bewijzen/2012-13/feedback/Oven-deel1 +	Jullie specificatie van het geheel bestaat uit drie zinnen. Dus dan verwacht ik een ∧-formule met drie onderdelen waarvan elk stuk precies een zin is. Nu wordt de desda uit de eerste zin ook gekoppeld aan het piepen uit de derde zin. Verder gebruiken jullie hier opeens predikaten als 'IsVerhitTot' en 'WekkerPiept' die niet in het domeinmodel en het netwerk staan. Ook is de syntax niet correct. En er wordt een s gebruikt al voordat de kwantor ∀ s geweest is. In zijn algemeenheid lijkt hij slecht te assen bij de rest van het werkstuk. Qua gebruik van prredikaten, maar ook qua bewijsbaarheid als onderdeel van de correctheidsstelling.  +
Beweren en bewijzen/2012-13/feedback/Oven-deel1-her +	En als de gebruiker hier nu voor t2 -1 neemt? Klopt jullie stelling dan? Sowieso lijkt het met de hulpdefinities alsof er wordt uitgegaan dat t1<=t2, maar dat is denk ik niet het geval. Ik vermoed dat t1 de echte tijd is en t2 bijvoorbeeld de duur van 20 minuten. Dan weet je helemaal niet of [t1,t2] wel een zinnig interval is. Wel kun je dan praten over [t1, t1+t2]. Check svp al die hulpdefinities hierop. Verder zou ik verwachten dat er bijvoorbeeld ook iets als c2<c1 bij moet. En die voor alle t3 die precies op 1 t3 wordt beperkt zou misschien ook mooier met een exists kunnen. Of misschien beter nog, gewoon weg en op alle plaatsen waar nu t3 staat, dan t1+(c2-c1) schrijven. Persoonlijk denk ik dat deze specificatie van het geheel niet te bewijzen is uit de huidige onderdelen, maar ik vind het natuurlijk prima als jullie kunnen laten zien dat het wel kan! Succes!  +
Beweren en bewijzen/2012-13/feedback/Oven-deel2 +	De eerste helft van de specificatie van het geheel lijkt wel verdacht veel op het Wekker-onderdeel waardoor het bewijs hiervan wel niet zo ingewikkeld zal zijn. Ook hier ontbreken haakjes! Er is sowieso wel wat misgegaan gezien de html-entities die leesbaar zijn in de afdruk.  +
Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel1 +	De plaatsing van de ∀ x is heel raar. Er staat een heel stuk dat onafhankelijk is van x achter die ∀ en dat is verdacht. Gebruik Davids systematische methode om een goede formule te krijgen. Begin met de spec in natuurlijke taal in korte correcte stukjes op te knippen. Zo staat dat stukje over het branden van de LED heel raar. Is dat nu een vereiste voor het geschoren zijn? Of is dit toevallig ook een van de eigenschappen van het systeem, maar niet direct van belang voor het geschoren zijn? Het is vragen om problemen om zomaar in een klein stukje van een complexe formule opeens een desda te schrijven. Misschien kan een hulpdefinitie 'klaarOmTeScheren' hierbij handig zijn...  +
Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel1-her +	Jullie eerste eigenschap is tamelijk triviaal te bewijzen. Maar dat komt doordat die Mesjes zo'n krachtig onderdeel zijn. De andere twee eigenschappen kun je denk ik niet bewijzen. Dit komt vermoedelijk door de foute spec bij de accu.  +
Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel2 +	Wel dient er te worden opgemerkt dat er behoorlijk wat hulp aan docenten is gevraagd.  +
Beweren en bewijzen/2012-13/feedback/Slagboom-deel1 +	In de natuurlijke taal staat dat 'de slagboom geopend is'. Maar niet wanneer. En was het niet zo dat als er bijvoorbeeld een ticket gebruikt moet worden, dat minimaal 2 sec duurde? In de formule zie ik een 'grote of' staan. Is dat echt een of? Of moeten beide situaties gelden? In de natuurlijke taal zie ik alleen een 'kleine of' tussen knop ingedrukt of pas voor de lezer. Waarom dat verschil tussen natuurlijke taal en formule? Waarom hier wel toelichting op de naamgeving van de tijden?  +
Beweren en bewijzen/2012-13/feedback/Supermarkt zelfscanner-deel1 +	Voor dit tijdstip vind ik dat jullie voldoende ver zijn gekomen, maar voor de definitieve versie moet er nog duidelijke verbetering komen. In de tekst noemen jullie de interne computer, die voor het externe gedrag niet relevant is: als ik de scanner van buiten bekijk, zie ik niets van de interne computer. Je moet dus alleen dingen noemen die aan de buitenkant van de scanner zicht- of meetbaar zijn. Wel correct is het dat je noemt dat het totaalbedrag zonodig wordt doorgegeven aan de betaalautomaat, omdat jullie hebben bepaald dat de betaalautomaat geen onderdeel van het systeem is. Is „knop_ingedrukt” een externe invoer? Het is duidelijker als je de kwantor voor t2 plaatst bij het deel van de specificatie dat ook echt gebruik maakt van die variabele.  +
Beweren en bewijzen/2012-13/feedback/Supermarkt zelfscanner-deel2 +	De specificatie van het geheel wijkt af van de specificatie in het Coq-script. Wordt er op tijdstip t of op tijdstip (t+1) een boodschap op het beeldscherm afgedrukt? Het is beter het bereik van een kwantor alleen zover te laten lopen als nodig: Nu loopt het bereik van ∀ t:T, en van ∀ t2:T, over de hele formule, terwijl de eerste helft t2 niet gebruikt en de tweede helft t niet gebruikt.  +
Beweren en bewijzen/2012-13/feedback/stofzuiger-deel1 +	De specificatie van het geheel doet niets met „de stofzuiger is aangesloten op 230 V” of met „er zit stoflucht in de zuigerkop”. Bij volle_stofzak ontbreekt een parameter. De equivalentie kun je niet bewijzen; immers, de onderdelen garanderen alleen dat onder bepaalde voorwaarden een volle stofzak ontstaat, niet dat elke volle stofzak op die wijze ontstaat. Vervang de equivalentie door een implicatie.  +
Beweren en bewijzen/2012-13/feedback/verwarmingsysteem-deel1 +	De specificatie moet zijn: Als de ingestelde temperatuur hoger is dan de kamertemperatuur en de ingestelde temperatuur de komende ... uren niet wijzigt, dan ... De specificatie van de radiator moet nog uitgebreid worden, zodat je de eigenschap ook echt kunt bewijzen; op dit moment zegt de specificatie van de radiator alleen dat de watertemperatuur afneemt, zonder te zeggen dat (en hoe snel) de kamertemperatuur toeneemt.  +
Beweren en bewijzen/2012-13/feedback/vriezer-deel1 +	Plaats openende en sluitende haakjes, als ze op verschillende regels staan, precies onder elkaar, evenver ingesprongen als de operator die ze omsluiten. Dan zie je beter welke haakjes bij elkaar horen. De haakjes om „Instelling_waarde < Temperatuur” zijn overbodig.  +
Beweren en bewijzen/2012-13/feedback/vriezer-deel1-her +	Het is prima dat je „ingesteldeTemperatuurOpTijd” afkort met „ingesteld”, maar dan blijft het type hetzelfde. Ook bij „ingesteld” moet je dus een tijdsparameter opgeven (bv. in de specificatie van het geheel). Als je dat gecorrigeerd hebt, is de specificatie van het geheel goed.  +
Beweren en bewijzen/2012-13/feedback/vriezer-deel2 +	Ik neem hier ook het scenario mee; daar ontbreekt een korte uitleg wat de bedoeling ervan is.  +
Beweren en bewijzen/2013-14/feedback/Carwash-deel1 +	De laatste kwantor „&exists; t2:T,” is een existentiële kwantor, daar past geen implicatie bij. Het zou een ∀ moeten zijn. Bij „lichtAan” ontbreekt een parameter. Of „het juiste bedrag” is betaald, wordt niet gecontroleerd, maar alleen of het mogelijk is het juiste bedrag te betalen: „Er bestaat een geldbedrag dat het juiste is.”  +
Beweren en bewijzen/2013-14/feedback/Carwash-deel1-her +	Ik begrijp dat de auto op *elk* tijdstip na t3 schoon is. In het bijzonder is de auto op tijdstip t3+0.000000000000001 schoon. En ook op t3+100000000000000000. Echt waar? Je zult bedoelen: er bestaat een tijdstip t4 > t3, waarop de auto schoon is. Probeer het bereik van de kwantoren te verkleinen, bv. spreek je alleen in een klein deel van de formule over geld. Veel problemen kun je vermijden door eerst eens de specificatie als ''goede'' nederlandse zin op te schrijven, zoiets als: „Als de klant een programma kiest op een bepaald tijdstip en binnen een minuut voldoende geld betaalt en ..., dan is op een later tijdstip de auto schoon.” Daarna moet je die zin ''systematisch'' naar een formule vertalen.  +
Beweren en bewijzen/2013-14/feedback/Cruisecontrol-deel1 +	Er ontbreken haakjes in de formule, en ze is ook onzinnig. Het lijkt erop dat „goedeSnelheidEnAfstand t” alleen gegarandeerd wordt als zowel „gevaarlijkeAfstand t” als ook „~gevaarlijkeAfstand t” gelden. Ja, dát bewijzen is heel makkelijk. Bovendien past deze specificatie van het geheel niet bij de specificatie die je aan het begin van het werkstuk hebt gegeven.  +
Beweren en bewijzen/2013-14/feedback/Cruisecontrol-deel2 +	Na de specificatie van ’t geheel, in het axioma gasGelijk, staat na <tt>forall g:P,</tt> een conjunctie. Dat zou een implicatie moeten zijn. Een aantal van de axioma’s is overbodig omdat lin_solve dezelfde berekeningen kan uitvoeren.  +
Beweren en bewijzen/2013-14/feedback/De Game-deel 1 +	Signaal, toon_winst en toon_verlies zijn geen externe in- of uitvoersignalen van het hele systeem.  +
Beweren en bewijzen/2013-14/feedback/De Game-deel1-her +	De kwantor <tt>∃ k:K,</tt> lijkt me geheel overbodig omdat je de variabele <tt>k</tt> nergens meer gebruikt. Ook hier haakjes toevoegen: <tt>Signaal t (svk (Ctrl_knop_invoer t))</tt>. <tt>Signaal</tt>, <tt>toon_winst</tt> en <tt>toon_verlies</tt> zijn daarnaast geen invoer van het systeem als geheel, volgens het functionele netwerk. Dit schreef ik ook al bij de eerste beoordeling.  +
Beweren en bewijzen/2013-14/feedback/NS in- uitcheck paal-deel1 +	Geen specificatie in natuurlijke taal. Na een existentiële kwantor plaats je (normaliter) geen implicatie. Deze specificatie is, zelfs na correctie van deze fout, erg zwak: Als er een kaart getoond wordt, dan reageert het paaltje. Het mag bv. de incheckpiep laten horen, rood knipperen en schrijven dat je bent uitgecheckt. Het mag alles doen met de kaart wat het wil – daaraan wordt geen enkele eis gesteld.  +
Beweren en bewijzen/2013-14/feedback/NS in- uitcheck paal-deel2 +	Deze specificatie is nog steeds niet erg sterk: Als er een kaart getoond wordt, dan reageert het paaltje consistent. (Dit is een verbetering t.o.v. de eerdere versie.) Maar het paaltje mag nog steeds alles doen met de kaart wat het wil – daaraan wordt geen enkele eis gesteld. Het mag bv. een al ingecheckte kaart nog eens inchecken, of een foutmelding tonen terwijl de kaart helemaal in orde is.  +
Beweren en bewijzen/2013-14/feedback/NS in- uitcheckpaal-deel2-her +	(hier neem ik ook het scenario mee) Ongeveer de helft van de haakjes zijn overbodig.  +
Beweren en bewijzen/2013-14/feedback/Schiphol Bagage Sorteersysteem-deel2 +	„Alle bagage die in het systeem komt” → „Alle bagage die op tijd (d.w.z. minstens 27 minuten voor vertrek) in het systeem aankomt”  +
Beweren en bewijzen/2013-14/feedback/Sluis-deel1 +	alleen in natuurlijke taal. Ik wil ook graag een formule zien die de vertaling is van jullie zin. Ik zie niet hoe je met deze onderdeelspecificaties iets kunt zeggen over boten in de sluis. Je moet óf het doel bijstellen en alleen zeggen dat de sluisdeuren afwisselend openen (zodat boten, als ze toevallig in de buurt zijn, ervan gebruik kunnen maken) óf de formules bijstellen, een type van boten toevoegen en eigenschappen van boten toevoegen (bv. een boot vaart wel door als de deur open is, maar blijft waar hij is als de deur dicht is), zodat je dan kunt zeggen „Elke boot die voor de sluis ligt (en zich aan de aanwijzingen houdt), ligt na een aantal minuten achter de sluis.”  +
Beweren en bewijzen/2013-14/feedback/Sluis-deel1-her +	De nederlandse zin zegt nog iets meer dan de formule: „dan is deze boot tussen de tijdstippen t+13 minuten en t+27 minuten uit de sluis”. Overigens moet je ergens nog de aanname toevoegen dat het verval maximaal 4m is.  +
Beweren en bewijzen/2013-14/feedback/Stoplichtensysteem-deel2 +	Vanwege het inexacte domeinmodel stel je inconsistente eisen: Enerzijds wordt in <tt>AutosRijdenDoor</tt> gerekend met de definitie zoals door jou gegeven, en anderzijds wordt in <tt>AutosVerdwijnenNiet</tt> gerekend met de definitie zoals ik hem heb gegeven. Ik kan uit de twee formules concluderen: Als een auto op de druksensor staat te wachten, dan blijft hij daar voor altijd wachten. Immers, zodra het betreffende stoplicht op groen zou springen, ontstaat een tegenspraak. In het bewijs heb je, voorzover ik het kon ontdekken, deze tegenspraak niet uitgebuit.  +
Beweren en bewijzen/2013-14/feedback/achtbaan-deel1 +	Ook hier weer syntaxfouten, maar die hebben jullie in het Coq-script al opgelost. Echter, ik denk dat deze eigenschap niet te bewijzen is. Ik heb namelijk geen enkel onderdeel gezien dat er voor zorgt dat de trein weer terug komt bij het Station. En dat heeft wel te maken met jullie inconsistentie over het al dan niet modelleren avn de hele baan. Verder denk ik dat deze stelling wel eens te simpel kan zijn. (Afgezien van het vorige probleem natuurlijk.) En waarom 'moet' de trein rijden voor 59 seconden? Jullie werken in R, dus 59.9 seconden is toch ook goed?  +
Beweren en bewijzen/2013-14/feedback/achtbaan-deel1-her +	Ook hier is de layout van de formule gewoon niet goed. En zitten er ook syntaxfouten in. Zie bijvoorbeeld de ∀ u:T. Daar moet echt een haakje voor. Net zo bij die ∀ v:T verder naar beneden.  +
Beweren en bewijzen/2013-14/feedback/achtbaan-deel2 +	Om te beginnen is de layout bijzonder onduidelijk. Door de vele pijlen en het feit dat de spec niet op 1 pagina staat is moeilijk te zien welke haakjes nu bij elkaar horen en op welk niveau de pijlen precies staan. De beste manier om dit op te lossen is om losse definities met verstandige namen te maken zodat zo'n hele '&neg;∃' in een zin kan worden beschreven. Eigenlijk lijkt dit heel sterk op wat er in het bewijs gebeurt. Daar bedenken jullie namen van aannames als 'baanvrij' en 'noodbeugels' en diezelfde namen hadden jullie hier natuurlijk ook kunnen gebruiken. Verder is het een beetje een gemiste kans dat het verplaatsen naar het station op precies dezelfde manier lijkt te gaan als in onderdeel Baan. Het zou me niet verbazen als jullie daardoor niet eens de definitie van garandeerAanwezigheid hoeven open te vouwen.  +
Beweren en bewijzen/2013-14/feedback/alarmsysteem-deel1 +	In de spec van Alarmsysteem3 en Alarmsysteem4 zit een foutje. In de natuurlijke taal komt de u helemaal niet voor en in de formule is er ook iets mee waardoor deze twee eigenschappen nu niet te bewijzen zijn.  +
Beweren en bewijzen/2013-14/feedback/automatischlicht-deel1 +	Er gaat iets mis met de scope van t10. Die wordt volgens mij aan het eind van de regel afgesloten, maar daarna wordt hij weer gebruikt. Dus misschien moet dat daar geen t10 zijn. Verder denk ik dat jullie eigenschap niet te bewijzen is met de huidige onderdelen. Teken eens een tijdlijn en bekijk op welk moment je moet hebben dat beweging_gedetecteerd is en op welk moment je dat weet uit de aannames. De manier waarop de intervallen staan in LichtRegelaar en in de spec van het geheel is net anders. En daardoor waarschijnlijk net fout. Enerzijds moet het er wel op lijken, maar ook weer niet zo veel dat het bewijs triviaal wordt.  +
Beweren en bewijzen/2013-14/feedback/automatischlicht-deel1-her +	Hier zitten natuurlijk dezelfde fouten in als in de onderdelen met betrekking tot ∨, ∧ en →. Verder zit er volgens mij een rekenfout in jullie systeem. Als ik namelijk de fouten met de of, en en pijl verbeter en de stelling probeer te bewijzen, moet ik hebben dat er 15 minuten lang spanning is, terwijl er maar 10 gegeven zijn. Schijnbaar wordt er in het systeem drie keer iets afgeschat met 5 minuten extra in plaats van twee keer. Door die 10 in 15 te veranderen, kon ik de stelling wel bewijzen. Het bewijs ging wel makkelijk, maar is niet triviaal door al die intervallen.  +
Beweren en bewijzen/2013-14/feedback/automatischlicht-deel2 +	Ook hier dezelfde fout met de layout. Verder ontbreken er haakjes bij de kwantoren. Haakjes die Coq niet nodig vindt, maar onze grammatica wel.  +
Beweren en bewijzen/2013-14/feedback/betterplace-deel1 +	Op zich is dit wel het soort specificatie van het geheel dat je wil hebben. Een eigenschap die niet precies hetzelfde is als de specs van de onderdelen, maar wel bewijsbaar is. Helaas is hij niet bewijsbaar, want ik zie bijvoorbeeld niet hoe Pas_geld en Pas_check ooit waar kunnen worden uit deze aannames.  +
Beweren en bewijzen/2013-14/feedback/betterplace-deel1-her +	Deze eigenschap geeft goed weer wat er aan de hand is. Als je alleen maar vertelt dat er een pas is, kan het zo zijn dat het allemaal in orde is en dan wordt de accu vervangen of dat er iets niet in orde is en dan moet de auto linksaf.  +
Beweren en bewijzen/2013-14/feedback/bloeddrukmeter-deel1 +	Met al die onderdelen erin ziet dit er meer uit als een correctheidsstelling dan als een spec van het geheel! Wat jullie als natuurlijke taal hebben gegeven lijkt veel meer op een specificatie van het geheel dan de formule.  +
Beweren en bewijzen/2013-14/feedback/bloeddrukmeter-deel1-her +	Ik denk dat jullie hier veel te weinig eisen. In welk interval is er precies stroom nodig? En wanneer luchtinlaat? En wanneer moet hij om de arm zitten?  +
Beweren en bewijzen/2013-14/feedback/boormachine-deel1 +	Zelfde verhaal. In de formule staat van alles over de hendel en stroom die gedurende een bepaalde tijd iets moeten doen. Maar in de natuurlijke taal komt daar niets van terug. Verder is het zo dat deze formule bijna letterlijk gelijk is aan de formules van de onderdelen. In het bijzonder wordt daardoor het bewijs veel te simpel. Als je een bewijs kunt maken met grofweg alleen maar all_e, imp_e en con_i, kan ik je op een briefje geven dat dat geen voldoende cijfer oplevert. De truc is om in de specificatie van het geheel juist net andere getallen te gebruiken dan in de specs van de onderdelen, maar wel zo dat de eigenschap waar is. Bijvoorbeeld als je Boorkop tevreden is met 10 seconden boren, zeg dan in de spec van het geheel dat je 12 seconden lang boort. En als je weet dat je in 10 seconden precies x cm diep gaat, zeg dan in de spec van het geheel dat als je 12 seconden boort dat je dan minstens x cm diep zit. Je hebt een aantal ∃-kwantoren in je formule staan, maar die gebruik je helemaal niet omdat ze links en rechts van de pijl hetzelfde zijn! Zorg dat je de ∃ uit de aannames met een exi_e daadwerkelijk moet uitpakken om dan in de &exits; uit de conclusie met een exi_i een goede waarde kunt aanwijzen.  +
Beweren en bewijzen/2013-14/feedback/boormachine-deel2 +	De formule is hier verbeterd, maar wederom is de natuurlijke taal achtergebleven. Als je deze specificatie van het geheel nog eens rustig leest, dan zie je toch hopelijk zelf ook dat dit geen zin is? "Als er een stuk hout ligt met een gat van 0 mm, de aan knop staat voor meer als 30 seconden stoom, er is stroom voor meer als 30 sec en de hendel is omlaag, dan wordt er een gat geboord." Nog afgezien van het feit dat er in de natuurlijke taal helemaal niets wordt gezegd over het feit dat door onnauwkeurigheid het gat net even iets groter kan zijn dan bedoeld.  +
Beweren en bewijzen/2013-14/feedback/breakfastmachine-deel1 +	Ik stel voor dat je het laatste deel verandert in: „Er bestaat een tijdstip waarop het ontbijt is geserveerd.”  +
Beweren en bewijzen/2013-14/feedback/breakfastmachine-deel2 +	Inhoudelijk is de specificatie in orde; ze bevat helaas syntaxfouten: het sluitende haakje dat bij <tt>(∃tr:C,</tt> hoort ontbreekt.  +
Beweren en bewijzen/2013-14/feedback/buizenpost-deel1 +	Zoals eerder reeds gezegd zou ik niet de huidige functies gebruiken, maar predikaten om de capsule en zijn bestemming in de spec te krijgen. Verder denk ik dat deze eigenschap niet te bewijzen is. Ik heb namelijk de indruk dat er geen enkele aanname is die garandeert dat de buis van s naar de centrale eenheid en de buis van de centrale eenheid naar getBestemming (getCapsule s) ooit beschikbaar komen. En dan wordt er volgens mij niets verstuurd. Dit kun je op verschillende manieren oplossen. Lelijk door een extern predikaat te maken dat in de spec van het geheel bij de aannames staat en dat dit garandeert. Mooier door bij het onderdeel dat het interne fenomeen buisBeschikbaar verzorgt, te laten garanderen dat elke buis ergens binnen 30 seconden beschikbaar komt. Dan weet je a priori niet hoe groot de u is uit jullie conclusie, maar je weet wel dat dat maximaal 60 seconden na t zal zijn. (Heb even niet gecheckt of er andere onderdelen zijn die nog wat vertraging introduceren.)  +
Beweren en bewijzen/2013-14/feedback/buizenpost-deel2 +	Op zich is dit wel in orde.  +
Beweren en bewijzen/2013-14/feedback/buizenpost-deel2-her +	Een tamelijk originele eigenschap van het systeem. Had de spec nog uitgebreid kunnen worden met de eigenschappen dat er ook capsules zijn die wel aankomen? Beetje jammer van die lege bak op t+2. Niet dat dat fout is, maar het ziet er een beetje raar uit. Om de een of andere reden ziet het er mooier uit als je zegt dat hij van t tot en met t+2 de hele tijd leeg is. (Maar ik weet niet of dat ook echt zo is, want anders krijg je natuurlijk een inconsistentie!)  +
Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel1 +	Ook hier weer: als t2 en t3 alleen maar vaste waarden (t1+1/100) zijn, heb je ze helemaal niet nodig. Als het iets uit een interval is heb je ze waarschijnlijk wel nodig. Echter, doordat jullie hier een ∀ bewering met ∧'s koppelen, staat hier volgens mij in het bijzonder dat voor alle t1 en t2 geldt dat t2>= t1+1/100. Maar dat is natuurlijk niet zo, want neem maar t2=t1...  +
Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel2 +	In jullie natuurlijke taal ontbreken wat 'en' woordjes tussen de verschillende regels in de 'als'. En ook het 'dan' deel is niet echt precies. En waarom staat die t3 al voor de pijl? In de natuurlijke taal staat alleen maar iets over dat interval bij de 'dan'.  +
Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel2-her +	Eigenlijk is het natuurlijk de bedoeling dat in een spec in natuurlijke taal die momenten als t1 en t1+3+2/100 niet meer voorkomen, maar worden uitgelegd met woorden als 'op een zeker moment' of '3.02 seconden na dat moment', maar in mijn mail met een suggestie over de spec van het geheel heb ik weliswaar gezegd dat dit een versimpelde versie was, maar niet duidelijk gezegd dat dat ook ging over die momenten, dus dat reken ik niet aan.  +
Beweren en bewijzen/2013-14/feedback/gokautomaat-deel1 +	Die 'drie opeenvolgende tijdstippen' klopt niet meer precies met de formule toch?  +
Beweren en bewijzen/2013-14/feedback/gokautomaat-deel2 +	Hoewel het wat onbevredigend is dat er geen tijdslimiet in zit en dat er zoveel kwantoren nodig zijn omdat er nu geen systeem is om aan te tonen dat als een schijf stil staat hij stil zal blijven staan totdat er weer geld wordt ingegooid en op de knop wordt gedrukt, is dit met de huidige specificaties van de onderdelen ongeveer het beste wat jullie er van kunnen maken.  +
Beweren en bewijzen/2013-14/feedback/hdd-deel1 +	Goed bedacht dat je lezen van data koppelt aan een eerdere schrijfactie. Zo hoef je alleen over fenomenen aan de buitenkant te spreken. Helaas is toch iets van het interne signaal „gData” ingeslopen. Ook hier zie ik vreemde indentatie van de formule en verkeerde haakjes (voor „forall t2:T,” moet een haakje staan). Klopt de disjunctie voor „pwrSignaal t = "write"”?  +
Beweren en bewijzen/2013-14/feedback/hdd-deel1-her +	De formule is geen vertaling van de zin in natuurlijke taal. Formuleer eerst een zin zonder variabelennamen (immers, ook de formule bevat geen vrije variabelen). Verbeter dat alsnog. Extra verwarrend is dat de vrije variabele t2 in de nederlandse zin bedoeld is om te verwijzen naar de gebonden variabele t in de formule en de vrije variabele t in de nederlanse zin zou moeten verwijzen naar de gebonden variabele t2 in de formule. (Helaas kan dat niet, omdat een vrije en een gebonden variabele nooit hetzelfde zijn. Zelfs als ze dezelfde naam hebben, zijn het twee verschillende variabelen.) Verbeter dat alsnog. Je kunt de zin ongeveer zo beginnen: „Op elk moment dat de controller stroom heeft geldt: 1. Als de controller op een dergelijk tijdstip moet lezen, dan ... 2. Als de controller op een dergelijk tijdstip moet schrijven, dan ...” Verbeter dat alsnog. Bovendien lijdt de specificatie van het geheel aan dezelfde euvels als de Draaischijf: een incorrecte subformule om uit te drukken dat de laatste geschreven gegevens gelezen worden, en twee verschillende variabelen t2. Verbeter dat alsnog. Zoals ik in het eerste commentaar al heb geschreven: De specificatie noemt het interne signaal „gData”. Dat mag niet. Verbeter dat alsnog.  +
Beweren en bewijzen/2013-14/feedback/homecinemaset-deel1 +	Zelfde fouten als bij de onderdeelspecificaties met kwantoren en haakjes. En zeker bij zo'n lange specificatie is het van belang om de spec in kleine overzichtelijke zinnen te knippen. Geef elke eigenschap een passende naam en maak definities van elk van die zinnen. Vervolgens bewijs je al die dingen afzonderlijk en laat je zien dat je met apply ook met lemma's en deelstellingen kunt werken.  +
Beweren en bewijzen/2013-14/feedback/homecinemaset-deel1-her +	Het goede is dat jullie eigenlijk twee specs van het geheel hebben. Een voor de Boxset en een voor het hele systeem. Het slechte is dat jullie stelling niet bewijsbaar is. Als je bijvoorbeeld Televisie wil bewijzen, heb je nodig dat 'tv_in t1 g1' geldt voor zekere t1 en g1 om beeld op te kunnen leveren. Maar daar wordt niet voor gezorgd. Ook niet positief is dat jullie stelling overal gewoon t+1 gebruikt. Daardoor wordt het bewijs niet ingewikkeld. Wat jullie zouden kunnen doen is om in de onderdelen die verschuiving van 1 seconden te veranderen in iets variabels, dus in iets als &exists; v met v in (0,3) en het resultaat wordt dan niet opgeleverd op t+1 maar op t+v.  +
Beweren en bewijzen/2013-14/feedback/homecinemaset-deel2 +	Mijn eerste gedachte is dat jullie systeem langzamer is dan jullie hier denken. Bij de TV zeggen jullie dat er binnen 3 seconden nadat er door de ontvanger beeld wordt ontvangen er beeld op de tv is en geluid uit de speakers komt. Maar zo'n beetje al jullie onderdelen kunnen 3 sec vertraging opleveren. Dus als twee onderdel na elkaar al 3 sec vertraging kunnen opleveren, kan het toch al 6 sec duren voor het signaal uit het tweede onderdeel komt? Verder eisen jullie alleen maar stroom op moment t, maar de TV heeft door die vertragingen pas veel later (nou ja, mogelijk enkele seconden) stroom nodig dan de ontvanger. Waarschijnlijk moeten jullie eisen dat vanaf moment t de apparaten allemaal zeker 20 sec stroom (zomaar een getal waarvan ik denk dat het alle vertragingen aan kan) nodig hebben. Krijgen jullie meteen nog een interval in het systeem. Wordt het spannender.  +
Beweren en bewijzen/2013-14/feedback/homecinemaset-deel2-her +	Hier zijn de adviezen gelukkig wel opgevolgd. Alleen denk ik niet dat ik thuis een systeem zou willen hebben waarbij het beeld en het geluid op verschillende tijden komen...  +
Beweren en bewijzen/2013-14/feedback/kentekenslagboom-deel1 +	Er is een overbodige gebonden variabele t2. Wat is de specificatie in natuurlijke taal? Wat gebeurt er onmiddellijk nadat de auto is verdwenen? Moet dan niet eerst de slagboom dicht voordat je ~beweegt t kunt concluderen? En als er een obstructie is, dan klinkt tien seconden lang geen alarm -- maar wat als er na die tien seconden nog steeds een obstructie is? Dan moet dus wéér tien seconden geen alarm klinken.  +
Beweren en bewijzen/2013-14/feedback/kentekenslagboom-deel2 +	In Kentekenslagboom2 zouden haakjes moeten staan om <tt>(forall k:K, ~dichtbij t k)</tt>. Dan betekent de formule echt „Als er geen auto dichtbij is ..., dan ...” Je huidige formules betekenen eerder zoiets als: „Voor elke auto geldt: wanneer hij niet dichtbij is en er geen obstructie is, dan is het alleen mogelijk dat de slagboom open is als hij onmiddellijk dichtgaat; anders is hij niet open.” Dus: als mijn auto niet dichtbij is, dan moet de slagboom onmiddellijk dicht, zelfs als jouw auto wel dichtbij is. De specificatie is bewijsbaar omdat je in de processor voorschrijft dat de slagboom, zolang er geen detectie is, niet open moet, onafhankelijk ervan of een auto dichtbij is of niet. Overigens heb je Kentekenslagboom2 in het Coq-script een tikje vereenvoudigd.  +
Beweren en bewijzen/2013-14/feedback/koffiezetapparaat-deel1 +	Ik denk niet dat dit hem gaat worden. Volgens mij eist jullie Warmhoudplaat toch dat er minimaal 30 seconden verwarmd is? Dus ik denk dat er ook minimaal die periode stroom moet zijn en zo. Terwijl jullie dat slechts op 1 moment geven. En jullie kwantificeren in natuurlijke taal over voor alle koffie. Maar koffie is helemaal geen verzameling in jullie domeinmodel. Wat bedoelen jullie hier precies?  +
Beweren en bewijzen/2013-14/feedback/koffiezetapparaat-deel2 +	Het ziet er een beetje raar uit dat jullie spanning_KA en KA_aan gedurende twee, gedeeltelijk (of helemaal?) overlappende intervallen eisen. Netter was geweest om in te zien dat jullie iets moesten doen met het maximum van filtertijd+verwerktijd en 30. Nu is er ogenschijnlijk een tamelijk eenvoudige stelling over gebleven.  +
Beweren en bewijzen/2013-14/feedback/kopieerapparaat-deel1 +	Gelukkig staat hier niet precies wanneer de kopie klaar is, maar alleen een interval. Desondanks lijkt me dit een tamelijk simpele stelling. Het zou waarschijnlijk helpen als jullie ook onderdelen gebruiken die niet precies zeggen wanneer wat klaar is. Zoals jullie al hebben bij de uitrolmotor. Overigens is deze eigenschap denk ik niet te bewijzen, want teken maar eens een tijdslijn en kijk op welk moment welk predikaat waar is (dan wel moet zijn). Volgens mij past dit niet precies.  +
Beweren en bewijzen/2013-14/feedback/kopieerapparaat-deel2 +	Hier zitten in elk geval twee ∃-kwnatoren in waardoor het bewijs iets spannender wordt. Verder denk ik dat jullie apparaat ook wel met iets minder strikte eisen zo'n kopie kan opleveren, want is het echt nodig dat de hele 15 seconden er papier en inkt aanwezig is?  +
Beweren en bewijzen/2013-14/feedback/pinautomaat-deel1 +	Een goed begin zo met die specifieke getallen. Als je het moeilijker (en mooier) wil maken, zeg je niet dat er een pincode op t+10 wordt ingetoetst, maar ergens in een interval (t+7, t+12). Netzo voor die andere momenten. Je kunt dan zelf uitrekenen binnen welk interval er uiteindelijk geld komt. Overigens denk ik dat deze eigenschap niet te bewijzen is. In natuurlijke taal zeggen jullie wel dat de code en pas moeten matchen, maar niet wanneer. En in de formule staat daar al helemaal niets over. Dus ik denk dat jullie database info te kort komt om het pinpascode_oke signaal te kunnen versturen. Iets soortgelijks voor het saldo.  +
Beweren en bewijzen/2013-14/feedback/pinautomaat-deel2 +	Hier staan een heleboel variabelen die na de pijl niet terugkomen. Maar dat betekent waarschijnlijk dat je dan geen ∀pc:PC hoef te doen, maar kunt volstaan met een &exists;pc:PC, waarvan de scope voor de pijl wordt afgesloten.  +
Beweren en bewijzen/2013-14/feedback/snoepautomaat-deel1 +	Ook hier de en/of-fout. Verder lijkt het allemaal wel heel erg op de onderdelen.  +
Beweren en bewijzen/2013-14/feedback/snoepautomaat-deel2 +	Maar hij lijkt wel heel sterk op de onderdelen. Zelfs de naamgeving van de verschillende momenten is gelijk.  +
Beweren en bewijzen/2013-14/feedback/stofzuiger-deel1 +	Enerzijds ziet de formule er veel te simpel uit. Alles gebeurt op tijdstip t. Desondanks denk ik dat jullie deze simpele eigenschap met deze onderdelen niet kunnen bewijzen. Verder komt het schoonmaken niet terug in jullie specificatie. Dit is misschien op te lossen door een ander predikaat dan zuiging te gebruiken. Misschien moeten jullie van die zuiging meer iets interns maken en een extra onderdeel vloer of ruimte toe te voegen, waarbij in dat onderdeel een soort specificatie komt als: indien er zoveel tijd gezogen wordt, dan is de vloer zoveel procent schoongemaakt.  +
Beweren en bewijzen/2013-14/feedback/tandenborstel-deel1 +	In jullie geazichtspunt zeggen jullie iets over het al dan niet 2 seconden geleden aangezet zijn van het ding als hij roteert. Maar daar zie ik bij jullie spec van het geheel niets van terug. Verder gebruiken jullie het interne fenomeen tijdslimiet_signaal in de spec van het geheel, terwijl je daar normaal gesproken alleen maar de externe fenomenen gebruikt.  +
Beweren en bewijzen/2013-14/feedback/tandenborstel-deel2 +	Het blijft een beetje onduidelijk wat er nu getoond wordt door display_rest_accu.  +
Beweren en bewijzen/2013-14/feedback/thuisalarmsysteem-deel1 +	Hier staan haakjes op de verkeerde plek. Verder is het zo dat deze spec van het geheel bijna letterlijk hetzelfde is als de spec van het onderdeel Contr_pan. Dat betekent dat er waarschijnlijk een te simpel bewijs uit komt. Probeer de spec van het geheel zo aan te passen dat hij wel volgt uit de onderdelen, maar dat er daarvoor wat werk moet worden gedaan om het te bewijzen, bijvoorbeeld via exi_e of interval en lin_solve.  +
Beweren en bewijzen/2013-14/feedback/thuisalarmsysteem-deel2 +	Hier zit dezelfde fout met de ∃ in als bij het Contr_pan.  +
Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel1 +	Op zich ziet het er niet heel erg gek uit qua eigenschap. Behalve dan dat jullie blijkbaar tevreden zijn met stroom aan het begin en zo in plaats van het hele interval. Verder ontbreken er haakjes rond de ∃d:C volgens de grammatica. Coq keurt dit misschien wel goed, maar interpreteert het anders dan jullie layout doet vermoeden! Het zou me verbazen als de huidige eigenschap te bewijzen is. Maak een tijdslijn en kijk op welk moment welk predikaat moet gelden.  +
Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel2 +	De natuurlijke taal is niet zo heel erg natuurlijk meer met functies als owt er in, maar het is natuurlijk ook iets ingewikkelds. Verder wordt hier over tijdstippen tx gesproken, maar dat zijn tijdsduren. Die aanname over niet-negatieve tijdsduren hadden jullie beter als een afzonderlijke Hypothesis kunnen opnemen. Nu staat het in de formule en dus ook op een rare manier in de natuurlijke taal.  +
Beweren en bewijzen/2013-14/feedback/walkietalkie-deel1 +	In natuurlijke taal hebben jullie het over een goede batterij, in de formule over batterij_geplaatst, maar ik neem aan dat jullie daar eigenlijk jullie hulpdefinitie willen gebruiken. (Anders is de eigenschap sowieso niet te bewijzen, want zonder kennis over het batterijniveau doet de Batterijhouder niets.) Verder zou ik de eigenschappen anders weergeven. Jullie hebben nu je best gedaan om alles onder 1 ∀t te doen, maar dan zie je dat er in de natuurlijke taal als voegwoord tussen twee zinnen een 'of' staat terwijl er een 'en' in de formule staat. Zeker bij ingewikkelde eigenschappen kun je het beter in losse zinnen splitsen: * Als de aanknop is ingedrukt, er een goede batterij geplaatst is, de zendknop is ingedrukt en er een geluidssignaal binnenkomt op de microfoon, dan wordt er 100 milliseconden later een signaal verzonden naar de ether. * En als de aanknop is ingedrukt, er een goede batterij geplaatst is, de zendknop niet is ingedrukt en er een signaal uit de ether binnenkomt, dan komt er 50 milliseconden later een signaal uit de jack. * En als de jack niet is aangesloten en er een zekere tijd later een signaal uit de jack komt, dan komt er weer 50 milliseconden later ook geluid uit de speaker. (Deze laatste is natuurlijk niet precies wat jullie nu zeggen, maar zorgt ervoor dat jullie misschien wel iets met een exi_e-regel moeten laten zien.) Door de eigenschappen te splitsen krijg je makkelijkere zinnen om te vertalen naar formules en je krijgt een logische opsplitsing om het werk van het bewijs te verdelen! Wat verder mist is dat jullie eigenlijk niets eisen over die batterij. Een van de (sub)eigenschappen die ik zou verwachten is: * En als de aanknop 3 minuten lang op aan staat dan is het batterijniveau met 3 procent afgenomen (t.o.v. het maximale niveau), of is de batterij helemaal leeg. Ook heeft jullie definitie een parameter t en een ∀t; dat kan niet goed gaan.  +
Beweren en bewijzen/2013-14/feedback/walkietalkie-deel2 +	In het tweede geval wordt beweerd dat e rop precies t+125 iets uit de jack komt, maar de jack heeft een variabele vertraging, dus hoe gaat dat lukken? En in de formule staat er een d die niet gekwantificeerd is. Waarschijnlijk ontbreekt hier een ∃ d. Verder had WalkieTalkie eigenlijk natuurlijk als geparametriseerd onderdeel moeten worden vastgelegd. Dan is het daarna makkelijker om te zeggen dat er drie verschillende WalkieTalkies zijn die allemaal hetzelfde werken.  +
Beweren en bewijzen/2014-15/feedback/Airconditioner-deel1 +	Een tamelijk bescheiden specificatie, maar goed. Je maakt ook duidelijk hoe de vereenvoudigende aannames deze specificatie beïnvloeden. Wellicht moet je de specificatie een beetje wijzigen naar zoiets als „de temperatuur van de kamer is na ''maximaal'' 4 seconden 1 ºC lager”; het zou immers kunnen dat de airco al bezig is met koelen op het moment dat je bekijkt. (Een nog betere specificatie zou ongeveer zijn: Als de gewenste temperatuur niet hoger is dan de kamertemperatuur, dan is na verloop van tijd de kamertemperatuur verlaagd tot de gewenste temperatuur.)  +
Beweren en bewijzen/2014-15/feedback/Airconditioner-deel2 +	* Layout: de en-tekens en het pijltje kunnen eigenlijk nooit zo precies boven elkaar staan. * Er staat (* Aanname: de koelvloeistof die de compressor in komt is op kamertemperatuur. *) k_temp verdamper UIT t = temp kamer t. Maar bij die tekst had ik dan toch echt k_temp compressor IN t verwacht. * De natuurlijke taal spreekt over 4 seconden later, maar in de formule staat volgens mij heel iets anders.   +
Beweren en bewijzen/2014-15/feedback/Alarm-deel1 +	* Probeer in het definitieve werkstuk ervoor te zorgen dat de hele spec op 1 pagina staat! * Maar aangezien jullie toch al weten hoe hulpdefinities werken, kunnen jullie misschien beter drie simpele eigenschappen maken en die dan met /\ aan elkaar plakken in de spec van het geheel. ** Lampje brandt als er spanning is geweest. ** Alarm gaat af als de deur open is en er niet op tijd iets wordt uitgeschakeld. ** Alarm gaat af als er beweging is gedetecteerd en er niet op tijd iets is uitgeschakeld. * Gebruik intervalnotatie als jullie intervallen bedoelen. Dat maakt het beter leesbaar.   +
Beweren en bewijzen/2014-15/feedback/Arcadekast-deel1 +	Wellicht dat sommige equivalenties niet bewezen kunnen worden, om soortgelijke redenen als ik hierboven bij ak_gleuf heb beschreven. Bovendien hebben we in natuurlijke deductie geen bewijsregels voor equivalentie gegeven. Gebruik daarom implicaties.  +
Beweren en bewijzen/2014-15/feedback/Arcadekast-deel2 +	* Wel jammer dat er hier van al die desda's uit het gezichtspunt niets meer over is.   +
Beweren en bewijzen/2014-15/feedback/Auto-deel1 +	* 'Als er een situatie is waarin ...' is veel te vaag. Beschrijf die situaties precies, want dat moet in de formule ook. Sowieso kan de formule niet gecontroleerd worden als de natuurlijke taal vaag is. * wegdek_signaal_ok en weer_signaal_ok zijn interne fenomenen en horen dus niet thuis in de spec van het geheel. * Volgens mij staat hier nu dat de auto altijd remt. Want er wordt alleen maar gekeken of er een wegdek_signaal en zo zijn (en die zijn er altijd met jullie onderdelen?) en niet of de snelheid daar dan wel of niet bij past.   +
Beweren en bewijzen/2014-15/feedback/Autowasstraat-deel2 +	* Technisch gesproken is hij wel goed, maar hij is wel aan de erg simpele kant. Jullie hadden het bijvoorbeeld als iets moeilijker kunnen maken door in de stelling te zeggen dat er een moment tussen t+400 en t+500 is waarop de auto klaar is. Dan moet je een exi_i doen met (t+460) en bewijzen dat t+460 in [t+400,t+500] zit. Dus dan moeten jullie laten zien dat jullie die technieken beheersen. * Ook hadden jullie de onderdelen wat spannender kunnen maken door niet te zeggen dat zo'n onderdeel precies na 40 sec klaar is, maar ergens tussen de 37 en 42. Dan moet je ook een exi_e gebruiken in het bewijs.   +
Beweren en bewijzen/2014-15/feedback/De Ack-deel2 +	* Hier speel je een klein beetje vals. Connected is bijvoorbeeld afhankelijk van stroom, maar dat is een intern fenomeen. * Ook hier weer ontbrekende haakjes bij de exists.   +
Beweren en bewijzen/2014-15/feedback/Eierkoker-deel1 +	* Ook dit ziet er verdacht uit. De scope van ttijdens gaat over 'het' pijltje heen, terwijl ik denk dat jullie hem alleen maar voor de pijl nodig hebben om aan te geven dat gedurende een interval tussen tbegin en teind er aan allerlei eisen is voldaan. * En waarom wordt er in natuurlijke taal over 7 minuten gesproken terwijl ik alleen maar iets over 360 seconden zie?   +
Beweren en bewijzen/2014-15/feedback/Eierkoker-deel2 +	* De natuurlijke taal ontbreekt volledig. * Verder is het bijzonder onrealistisch. Jullie eisen alleen maar dat er op een zeker moment aan voorwaarden is voldaan en vervolgens zijn de eieren ooit klaar. Dit moet veel preciezer. Jullie eierkokers doen het thuis toch ook niet als je na het indrukken van de aanknop de stekker er uit trekt? * Enkele suggesties ter verbetering: ** Geef aan hoeveel eieren er zijn geplaatst en op welk tijdstip. Ergens voordat de knop is ingedrukt in elk geval. ** Geef aan hoeveel water er is geplaatst en op welk tijdstip. Ook weer ergens voordat de knop is ingedrukt. Jullie mogen zelf kiezen wat jullie eerst plaatsen: het water of de eieren, maar zorg dat die relatie dus wordt vastgelegd in de specificatie. ** Neem aan dat de hoeveelheid water die is toegevoegd voldoende is voor de hoeveelheid eieren. ** Gebruik een abstracte functie die aan de hand van de hoeveelheid eieren en de hoeveelheid water bepaalt hoe lang het duurt voordat de eieren moeten koken. Gebruik die functie in (ik denk) Container om een ondergrens aan te kunnen geven over die exists tuit.   +
Beweren en bewijzen/2014-15/feedback/Elektrische Tandenborstel-deel1 +	Moet ik de knop dus de hele tijd indrukken? De variabele m lijkt ook hier nauwelijks een functie te hebben. Als ik de nederlandse specificatie volg, had ik eerder zoiets verwacht als: forall t:T, forall m:TD, forall t2:T, t2 in [t, t+td] -> ... Overigens gaat deze tandenborstel na 120 seconden onophoudelijk piepen. Is dat de bedoeling? Of moet ze piepen 120 sec nadat de knop van niet-ingedrukt naar ingedrukt is veranderd? Dan moet je die verandering in de specificatie opnemen.  +
Beweren en bewijzen/2014-15/feedback/Elektrische Tandenborstel-deel2 +	* Maar het lijkt wel heel sterk op de specs van de onderdelen, dus ik ben benieuwd of jullie ook nog echt ergens intervallen moeten openknippen...   +
Beweren en bewijzen/2014-15/feedback/Elektronisch deurslot-deel1 +	* [ ] Ik snap het niet helemaal. Als ik dit lees maakt het helemaal niet uit welke gebruiker ergens op drukt, want het systeem doet altijd de deur open. * [ ] Ik zou hier wat verschillende eigenschappen verwachten: ** [ ] Als gebruiker g op knop openMijnDeur drukt dan zal zijn deur ergens binnen 10 seconden 5 seconden lang van het slot zijn en klinkt er een buzzer. (Die ergens binnen 10 seconden komt omdat bijvoorbeeld jullie app niet meteen het verzoek stuurt maar daar 1 seconde over kan doen. En misschien zijn er nog wel meer onderdelen die wat vertraging opleveren. In de spec van het geheel moet je gewoon zorgen dat je een interval neemt dat lang genoeg is voor alle vertragingen.) ** [ ] Als gebruiker g voor deur d staat en op de openDeur knop voor d drukt en de database van de server geeft aan dat g inderdaad deur d mag openen dan is er weer binnen 10 seconden een interval van 5 seconden waarbinnen de deur van het slot is en de buzzer gaat. * Zo kunnen jullie zelf misschien nog wat andere scenario's uitprogrammeren als specificatie.   +
Beweren en bewijzen/2014-15/feedback/Elektronisch deurslot-deel2 +	* Jullie maken hier dezelfde fouten met de intervallen. En daardoor wordt het dan uiteindelijk net weer bewijsbaar.   +
Beweren en bewijzen/2014-15/feedback/Gene gun-deel1 +	* Ogenschijnlijk ziet het er als een goede formule uit, maar dat is moeilijk te beoordelen want de natuurlijke taal mist. * Verder ziet het er een beetje simpel uit. * Zelfs zo simpel dat het denk ik niet te bewijzen is op deze manier. Ik zie namelijk geen enkele manier waarop de Rupturedisk ooit aan het werk wordt gezet. Nergens wordt gezegd wat de waarde van die drukken is. Wel dat ze veranderen, maar niet wat ze waren. Dus ik denk niet dat je dan kunt bewijzen dat ze ooit boven de 650 komen. * Verder geeft jullie input ook alleen maar aan dat op tijdstip t er aan bepaalde voorwaarden is voldaan. Dan geloof ik wel dat de Heliumpomp op tijdstip t+1 een hogere druk regelt. Maar wat als die nog niet goed genoeg is? Volgens mij kunnen jullie niet bewijzen dat hij op tijdstip t+2 een nog hogere druk heeft. * Zelfde probleem bij de vacuükamer denk ik.   +
Beweren en bewijzen/2014-15/feedback/Gene gun-deel2 +	* Waarom staat dat hele blok met forall k binnen de scope van die forall d? Die d wordt daar toch helemaal niet meer gebruikt?   +
Beweren en bewijzen/2014-15/feedback/Geschutstoren slagschip-deel1 +	In de formule lijkt het erop dat t1 buiten het bereik van de kwantor forall t1:T, staat. Dat is niet het geval, maar jullie moeten de indentatie aanpassen om te laten zien dat (forall t2:T, ...) ook onder het bereik van de eerste kwantor valt. In de nederlandse zin moeten geen variabelen voorkomen, net zoals in de formule ook geen vrije variabelen voorkomen. Wanneer vuurt het kanon? Volgens de specificatie is één keer springlading en „slaghoed” aanleveren voldoende om willekeurig vaak te vuren; dat zul je niet kunnen bewijzen.  +
Beweren en bewijzen/2014-15/feedback/Geschutstoren slagschip-deel2-her +	* Er staan allemaal interne fenomenen in de spec van het geheel. Hier moet alleen iets staan als 'als er op t1 dingen voorradig zijn en er op t2 signaal begin laden is geweest en op t4 signaal om te vuren dan vuurt het kanon op t5'.   +
Beweren en bewijzen/2014-15/feedback/Helikopter-deel1 +	Ik verwacht dat je de snelheden nog exacter moet opgeven. Je moet bovendien ook aangeven welke signalen níét gegeven worden, bv. dat tussen t+10 en t+45 de draaiknop niet naar rechts wordt gedraaid. Het is goed dat jullie een scenario gekozen hebben; dan wordt het bewijs nog interessant.  +
Beweren en bewijzen/2014-15/feedback/Helikopter-deel2 +	* Originele eigenschap. Goede uitleg hierover bij conclusie.   +
Beweren en bewijzen/2014-15/feedback/Lift-deel1 +	* Jullie weten blijkbaar niet het verschil tussen de specificatie van het geheel en de correctheidsstelling, want jullie zetten dit op de verkeerde plaats. * Ook hier weer exists-kwantoren voor pijlen, dus allemaal erg verdacht. * In de formule zie ik opeens getallen als 'binnen 5 minuten is er een lift aanwezig' maar die zie ik niet in de natuurlijke taal. Dat moet natuurlijk wel goed bij elkaar passen. * Jullie spec ziet er heel ingewikkeld uit, maar dat komt misschien doordat jullie alles in een formule proberen te stoppen. Misschien helpt het om de eigenschappen op te splitsen in simpelere formules (die elk hun eigen kwantoren hebben). ** Als er op een bepaald moment een verdieping wordt ingetoetst op een interface, dan verschijnt direct (misschien wel 1 seconde later) een liftletter op die zelfde interface die 3 seconden blijft staan en binnen 5 minuten (wel lang hoor; in 5 minuten (door)wandelen ben je ook op de 20e) is de aangegeven lift op deze verdieping. ** Als er (in het verleden) een bestemming is ingetoetst en de juiste lift is op de verdieping dan zijn de deuren zus en zo lang open en na zoveel tijd vertrekt de lift naar zijn bestemming. ** Als een lift vertrekt naar zijn bestemming dan komt hij daar aan na zoveel tijd... * Dit is maar een suggestie, misschien is het niet handig omdat je hierdoor misschien meer externe fenomenen nodig hebt. Maar jullie kunnen sowieso jullie spec verduidelijken door hulpdefinities te maken. Die zijn kleiner en makkelijker correct te krijgen. En vervolgens koppel je ze hier dan in de spec van het geheel met de juiste parameters aan elkaar.   +
Beweren en bewijzen/2014-15/feedback/Lift-deel2 +	* Dit was iets beter leesbaar geweest als jullie het hadden opgesplitst in kleinere stukjes. Ik denk dat er eigenlijk zoiets staat als: als op verdieping v1 wordt gevraagd om verdieping v2, dan is er een lift l die op verdieping v0 is en dan op tijdstip .... op verdieping v1 om vervolgens op tijdstip ... op verdieping v2 te zijn. Met folds en unfolds is dat in Coq dan makkelijker te overzien.   +
Beweren en bewijzen/2014-15/feedback/Pinautomaat-deel1 +	* Tikfout in de namen van de predikaten. * Waarom een dubbele pijl? * Hebben jullie de natuurlijke taal wel eens hardop gelezen? Kan dat zonder er over te struikelen? * Gezien het feit dat jullie verder alleen enkele pijlen gebruiken denk ik niet dat jullie deze dubbele pijl kunnen bewijzen.   +
Beweren en bewijzen/2014-15/feedback/Pinautomaat-deel2 +	* De natuurlijke taal ontbreekt volledig. * pincodeCorrect is intern en kan hier dus eigenlijk niet staan. * Verder is het een beetje raar dat al die acties precies 5 seconden na elkaar moeten worden uitgevoerd omdat het anders niet werkt. Dit is precies waarvoor existentiele kwantoren bedoeld zijn: er is een moment tussen t en t+15 waarop de pincode is ingevoerd... * En wat is het doe van die forall i:I? Die wordt verder nergens gebruikt.   +
Beweren en bewijzen/2014-15/feedback/PizzaAutomaat-deel1 +	ontbreekt  +
Beweren en bewijzen/2014-15/feedback/PizzaAutomaat-deel2 +	* Jullie gebruiken hier het interne fenomeen heeftBetaald. Jullie mogen alleen geldInname, knopVerlicht, knopDruk en pizzaUit gebruiken. * Waarom zit die derde regel binnen de scope van pr? Dat geld innemen is toch onafhankelijk van het pizzarecept? * Jullie maken in de spec van het geheel ongeveer dezelfde fouten als in de onderdelen, waardoor het vermoedelijk net in het bewijs weer goed komt.   +
Beweren en bewijzen/2014-15/feedback/Printer-deel1 +	De disjuncties moeten conjuncties worden. Volgens deze formule mag de leverancier kiezen aan welke van de eisen hij voldoet; als tenminste één functie werkt, voldoet hij aan de specificatie. Jullie bedoelen echter: Alleen als alle drie functies van een apparaat werken, is het een alles-in-één-printer. De specificatie in natuurlijke taal is erg onelegant. Ik denk dat het ook beter wordt als je duidelijker structureert in de drie functies (net als ik bij de processor voorgesteld heb), en je hoeft niet zo expliciet te beginnen met „voor al het papier ... geldt”.  +
Beweren en bewijzen/2014-15/feedback/Printer-deel2 +	* Jullie spec van het geheel lijkt sterk op de spec van de processor. Dus waarschijnlijk is dit wel bewijsbaar.   +
Beweren en bewijzen/2014-15/feedback/Sluis-deel1 +	In principe is de specificatie van het geheel wel (enigzins) correct. Echter, met deze specificatie zal het bewijs een heel eenvoudige en saaie oefening worden. Ik wil graag twee eigenschappen bewezen zien: # De schutsluisbesturing werkt veilig: Nooit geeft ze commando om beide deuren tegelijk te openen (of bijna tegelijk, als we rekening houden met de tijd die een deur nodig heeft om te openen en te sluiten), en nooit geeft ze commando om beide kleppen tegelijk te openen. Dit geldt tenzij de waterniveaus aan beide kanten gelijk zijn. # Als een schip binnen ... sec de sluis invaart (zodra hij open is) en binnen ... sec de sluis uitvaart (zodra de andere kant open is), dan duurt het schutten maximaal ... min. Voor deze eigenschappen zul je de specificaties van de onderdelen iets moeten uitbreiden.  +
Beweren en bewijzen/2014-15/feedback/Sluis-deel2 +	* De spec van het geheel lijkt verdacht veel op die van de Besturingskast, behalve dan dat alle interne fenomenen nu vervangen zijn door de externe varianten (al dan niet via functies). Dus ik geloof wel dat dit te bewijzen is. Maar ik geloof niet dat dit ingewikkeld is om te bewijzen.   +
Beweren en bewijzen/2014-15/feedback/Stereo-deel1 +	* **Er staat alleen een specificatie van het geheel in natuurlijke taal, maar er had er ook een in formules moeten staan! Of in elk geval een probeersel, eventueel voorzien van tekst waaruit blijkt waarom het nog niet gelukt is om echt een formule te geven.   +
Beweren en bewijzen/2014-15/feedback/Stereo-deel1-her +	* Ook hier weer alle kwantoren vooraan. * En ook weer een exists met een pijl. * En als in het tweede deel c altijd radio moet zijn, schrijf dan gewoon radio ipv forall c:C, c=radio.   +
Beweren en bewijzen/2014-15/feedback/Stereo-deel2 +	* Ook hier staan weer alle kwantoren vooraan, terwijl die of-reeks alleen maar van c en t afhankelijk is.   +
Beweren en bewijzen/2014-15/feedback/Thermostaat-deel1 +	In de formule zie ik niets terug van de zinsnede „en de temperatuur onder de gewenste temperatuur zit”.  +
Beweren en bewijzen/2014-15/feedback/Thermostaat-deel2 +	* De spec lijkt niet op de natuurlijke taal. * Verder gaat er iets mis met de scope van c. Eerst wordt c als Temp geintroduceerd, maar later als tijdstip ingevoerd in de functie Temperatuur. * Verder komt hier het predikaat Temperatuur_Meten dat niet in het domeinmodel staat. Ik denk dat jullie hier iets bedoelen als 'exists c:Temp, c = Temperatuur t'. * Die Verwarmen is een intern fenomeen en kan dus niet in de spec van het geheel gebruikt worden. Verder zou hij volgens de natuurlijke taal volgens mij na de pijl moeten. * Volgens mij kunnen jullie beter een concreet scenario proberen te bewijzen: Als de thermostaat is ingesteld op [06:00,09:00] op temperatuur 18 graden en om 05:30 is de temperatuur 12 graden, dan is er een moment tussen [06:30,07:30] waarop de temperatuur inderdaad 18 graden is. * Maar zoiets kunnen jullie nu niet bewijzen omdat er volgens mij niets is dat de temperatuur ook echt omhoog brengt als het predikaat 'Verwarmen' waar is. (Dat zou de kamer misschien kunnen doen? Iets als voor elke 15 minuten dat Verwarmen waar is, wordt de temperatuur met 1 graad verhoogd.) * Uiteraard zijn de getallen die ik hier noem slechts voorbeelden.   +
Beweren en bewijzen/2014-15/feedback/Thermostaat-deel3 +	Origineel scenario.  +
Beweren en bewijzen/2014-15/feedback/Wekkerradio-deel1 +	* Eigenlijk hebben jullie twee eigenschappen. Iets over het al dan niet afgaan van de wekker en iets over wat er op het display staat. Dat zit nu gecombineerd achter een forall fm:FM, maar ik denk dat die niet van belang is voor dat display. Jullie kunnen die dan ook beter als losse eigenschappen beschouwen en als (eig1) /\ (eig2) formuleren waarbij de benodigde kwantoren pas bij eig1 of eig2 worden geïntroduceerd. Eigenlijk precies conform de systematische vertaling. * Verder zou het voor de leesbaarheid wel helpen als jullie hulpdefinities gebruiken die met een goedgekozen naam een bepaalde situatie beschrijven. * Verder staan hier meer exists in dan ik zou verwachten. In het bijzonder lijken er onderaan wat combinaties van exists en -> te staan. En dat is altijd verdacht.   +
Beweren en bewijzen/2014-15/feedback/Wekkerradio-deel2 +	* In jullie natuurlijke taal staat een dan en slechts dan, maar waar staat die in de formule? * De layout met al die pijlen recht onder elkaar is eigenlijk niet volgens de criteria voor opmaak van formules. * Waarom staat die tijdnu in de scope van exists instellen? Zelfde voor exists tijdsnooze.   +
Beweren en bewijzen/2014-15/feedback/Zelfrijdende auto-deel1 +	eenvoudige variatie van de specificatie van de computer.  +
Beweren en bewijzen/2014-15/feedback/Zelfrijdende auto-deel2 +	* De natuurlijke taal bestaat uit een serie losse zinnen. Dit had dus ook echt per hulpdefinitie moeten worden weergegeven om enigszins zekerheid te hebben dat de (niet afgedrukte) formules kloppen. * In het bijzonder kan ik nu ook niet echt goed zien of de spec van het geheel nagenoeg gelijk is aan die van Computer, afgezien van interne/externe fenomenen.   +
Beweren en bewijzen/2014-15/feedback/domotica-systeem-deel1 +	* Je spec in natuurlijke taal is natuurlijk veel te simpel. Zorg dat je netjes beschrijft welke input welk gevolg op welk moment verzorgt. Verder heb ik mijn twijfels over al die of-tekens. Het is toch niet voldoende dat slechts een van die dingen werkt?   +
Beweren en bewijzen/2014-15/feedback/domotica-systeem-deel1-her +	* Nog steeds lijkt alles op moment t te gebeuren.   +
Beweren en bewijzen/2014-15/feedback/domotica-systeem-deel3 +	* Jammer dat je aannames zo sterk lijken op de onderdelen. * Je had bijvoorbeeld de "touch_invoer t i \/ spraakinvoer t i" om kunnen draaien, want dan moet je enkele dis_{e,i1,i2} toepassen die nu niet nodig zijn. * Ook de exists van de lichtsensor is hier weer precies "l < 100". Maar als je had gezegd dat er een was die kleiner was dan 78 had je later kunnen aantonen dat je weet hoe je Coq laat zien dat 78<100 is. * Net zo voor het interval van de timer. Had je hier een interval van 1800 seconden genomen, dan was de stelling nog steeds waar, maar had je wel kunnen laten zien dat je met "interval" kunt werken.   +
Beweren en bewijzen/2014-15/feedback/friteuse-deel1 +	* De opmaak van de formule voldoet niet aan de eisen. De sluithaakjes staan bijvoorbeeld niet recht onder de openhaakjes. * Het lijkt alsof jullie nu iets hebben van de vorm forall c:C, eig1 /\ eig2, waarbij eig2 helemaal niet van die c afhankelijk is. * Het is dan meestal handiger in het bewijs om het zo te doen: (forall c:C, eig1) /\ eig2. * Verder zie ik hier exists voor pijlen staan. Dat ziet er altijd eng uit (al kan het goedkomen doordat er nog foralls achter staan). Weten jullie zeker dat je hier exists en geen forall nodig hebt? * Welke onderdelen gaan isGoedGegaard opleveren?   +
Beweren en bewijzen/2014-15/feedback/friteuse-deel1-her +	* Hier zitten dezelfde twijfelachtige exists in de formule, dus misschien komt het samen wel goed uit. * Al heb ik hier toch wel heel sterk het gevoel dat er een exists met een -> wordt gekoppeld en dat is vragen om problemen.   +
Beweren en bewijzen/2014-15/feedback/industriele robot-deel1 +	De specificatie is formeel juist, maar ze zegt veel te weinig. Ik wil ook dat de lasrobot een beweging uitvoert die bij de lasopdracht past.  +
Beweren en bewijzen/2014-15/feedback/koffieautomaat-deel1 +	* Als ik de natuurlijke taal lees, lijkt het al alsof ik allemaal details over de interne werking tegenkom. Dat kan natuurlijk niet want de spec van het geheel is in termen van externe fenomenen! * Dus hier verwacht is iets als: ** Als een gebruiker op een willekeurig moment een beker plaatst en een keuzeknop indrukt en het apparaat onder spanning staat en d elekbak niet vol is, dan is er na maximaal 15 seconden een kopje met de drank die hoort bij de gekozen knop. ** En als en gebruiker op een wilekeurig moment een keuzeknop indrukt zonder dat er een beker is geplaatst, komt binnen 1 seconde de melding 'plaats beker' op het scherm. ** En als de lekbak wel vol is dan ... * Ook hier kunnen jullie zelf meerdere scenario's uitprogrammeren als een specificatie. * Waarom staat die forall d zo vooraan in de formule? Zet hem pas op de plek wara je hem nodig hebt.   +
Beweren en bewijzen/2014-15/feedback/koffieautomaat-deel1-her +	* Wat is de scope van die exists t2? Nu gaat deze exists weer over een pijl heen en dat is vragen om problemen. * En die forall t3 is gekoppeld aan een /\ wat vast een -> moet zijn. * In jullie natuurlijke taal schrijven jullie 'of' maar in de formule 'en'. Die 'en' in de formule is goed... * Jullie claimen alleen maar dat er op moment t een melding over de beker op het scherm staat, terwijl jullie onderdeel ervoor zorgt dat er 5 seconden lang zo'n melding is. Hier kunnen jullie het bijvoorbeeld spannender maken. Als jullie in de spec van het geheel aangeven dat die melding er 3 seconden is (moet te bewijzen zijn als hij er eigenlijk 5 seconden is) hebben jullie echt de interval regels nodig om uit dat grotere interval een kleiner interval te bewijzen. * Jullie systeem lijkt nu te zeggen dat de lekbakvol is als het water niet tot aan een bepaalde grens is gekomen? Ik denk dat er ergens een 'niet' mist. Of te veel staat.   +
Beweren en bewijzen/2014-15/feedback/koffieautomaat-deel2 +	* De plek van de exists is raar. Nu maken jullie in feit een exists met een pijl combinatie. En dat is altijd verdacht. * Die exists blijkt ook niet echt uit de natuurlijke taal.   +
Beweren en bewijzen/2014-15/feedback/medicijnautomaat-deel1 +	Het bereik van de kwantor forall r:Rec is verkeerd en daarom eist deze specificatie dat het welkomstbericht ook getoond wordt op momenten dat er minstens één recept níét getoond wordt – in de praktijk dus altijd, zelfs als tegelijk een ander bericht getoond wordt.  +
Beweren en bewijzen/2014-15/feedback/medicijnautomaat-deel2 +	* Hier is nog blijven staan wat er gebeurt als er geen recept getoond is, maar dat nemen jullie verder niet mee in de stelling.   +
Beweren en bewijzen/2014-15/feedback/platenspeler-deel1 +	In de eerste specificatie eis je alleen dat de plaat aan het begin van het afspelen aanwezig is. Je schrijft wel in je vereenvoudigingen dat de gebruiker de plaat niet aanraakt tijdens het afspelen, maar dat komt niet terug in deze specificatie of enige andere formule. Ik geef de voorkeur aan de tweede specificatie, maar ook die klopt niet helemaal. Bij de tweede specificatie eis je dat op tijdstip t de arm niet beneden is, maar op elk tijdstip tussen t (inclusief) en t+1+duurPlaat p wel beneden is. Deze eis is inconsistent voor tijdstip t. Je moet de subformule die begint met de kwantor forall t1:T, aanpassen: Ze zou ongeveer moeten betekenen „Als gedurende een tijdsinterval van t tot enige tijd later de hele tijd een spanning van 230 V op de stroom-ingang van de platenspeler staat ..., dan staat gedurende een tijdsinterval van t (of t+1?) tot evenveel tijd later een spanning op de linker en rechter audio-uitgang van de platenspeler die past bij plaat p.” De formule wordt niet een kwantorformule die een implicatie bevat, maar een implicatie die twee kwantorformules bevat. (Voor „enige tijd later” kun je voor het gemak de duur van de plaat gebruiken, maar in principe zou ook een kortere tijd kunnen.)  +
Beweren en bewijzen/2014-15/feedback/platenspeler-deel2 +	* Hier staan eigenlijk dezelfde rare dingen als in de onderdelen. Dat vergroot natuurlijk de kans dat het allemaal bewezen kan worden. * Maar waarom staat hier nu nergens op welk toerental het ding is ingesteld?   +
Beweren en bewijzen/2014-15/feedback/stoplichten bij x-kruispunt-deel1 +	* Waar is de natuurlijke taal? * In de Focus staat bij gezichtspunt als het goed is een niet zo gedetailleerde versie van deze spec. Maar bij jullie staat daar iets over 44 seconden en dat zie ik hier bijvoorbeeld niet terug. * En welk onderdeel gaat FunctioneerZndrConflict opleveren? Geen enkel toch? Dan is de stelling straks ook niet te bewijzen. * Aannames als autSignN u \/ ~autSignN u voegen niets toe want a\/~a kun je toch altijd met LEM bewijzen. * Nog afgezien van het feit dat jullie hier interne fenomenen gebruiken in plaats van de externe autAanN! * Ik denk dat het beter is om hier een of meerdere scenario's te schetsen: ** Stel dat er op tijd t een auto uit N komt terwijl op dat moment zijn licht op geel staat, en op tijd t-3 een auto uit W en ergens tussen t+3 en t+10 een auto uit Z en de hele (relevante) tijd geen auto uit O. Hoe lang duurt het dan maximaal voordat het licht voor de auto uit N op groen springt? ** Natuurlijk is het verstandig om eerst wat simpeler te beginnen: Stel op t komt er een auto uit N aan en zijn licht staat op rood en de minuut daarvoor en daarna komen er geen auto's aan uit de andere richtingen. Wanneer krijgt hij dan groen?   +
Beweren en bewijzen/2014-15/feedback/stoplichten bij x-kruispunt-deel3 +	Alleen hadden jullie de definities van de scenario's in natuurlijke taal dus hier moeten schrijven en niet bij focus.  +
Beweren en bewijzen/2014-15/feedback/tosti-ijzer-deel1 +	* Ik denk dat er haakjes missen waardoor die linker /\ anders bindt dan jullie denken. * Ik denk ook dat de kwantoren niet op de plek staan waar ze met de systematische methode zouden zijn gekomen.   +
Beweren en bewijzen/2014-15/feedback/tosti-ijzer-deel1-her +	* Geen natuurlijke taal? * De layout is ook niet conform de criteria van de leesbaarheid. In het bijzonder lijkt het nu als tostiijzer_warm de enige eis is voor lampje_aan, maar dat andere stuk tussen haakjes hoort er ook nog bij.   +
Beweren en bewijzen/2014-15/feedback/tosti-ijzer-deel2 +	* De natuurlijke taal past niet bij de formule. In de formule wordt voor een heel interval (waarom dit interval?) geeist dat er aan voorwaarden voldaan is.   +
Beweren en bewijzen/2014-15/feedback/vaatwasmachine-deel1 +	* De layout is niet volgens de criteria. Haakjes niet onder elkaar en de /\ en -> op het laatst staan verkeerd om. * Waarom precies vertellen wat de onderdelen nodig hebben? Dan krijg je straks een bewijs van de vorm A -> A en dat is niet ingewikkeld. Als je bijvoorbeeld hier eist dat de deur 33 minuten dicht is, terwijl het besturingssysteem maar 30 minuten nodig heeft, gaat het nog steeds werken, maar krijgen jullie de kans te laten zien dat jullie kunnen bewijzen dat als iets voor een langer interval geldt, het ook voor een korter interval geldt.   +
Beweren en bewijzen/2014-15/feedback/vaatwasmachine-deel2 +	* De natuurlijke taal zegt niets over tijden en de formule wel. * Verder ziet dit eruit als een eenvoudige stelling omdat de intervallen precies overeenkomen met die uit de onderdelen. Als je mee zou geven dat de deur bijvoorbeeld 33 minuten dicht zit, wordt de stelling al interessanter om te bewijzen. * Verder halen jullie wel vaat weg, maar wordt er nergens vaat toegevoegd...   +
Beweren en bewijzen/2014-15/feedback/voyager-deel1 +	* exists t:T gevolgd door een pijl? Jullie bedoelen vast dat dit voor alle momenten t moet gelden. * Ook hier weer dat gestabiliseerd een invoer is (lijkt) maar Propulsion_Subsystem lijkt het als uitvoer te beschouwen. * Sowieso snap ik die derde eis met de dubbele pijl niet. In de vierde eis staat toch al dat gestabiliseerd waar is? Dus dan betekent die dubbele pijl toch gewoon dat zon_zichtbaar en ster_zichtbaar waar zijn? * Die exists v op het einde is wat zwak. Het kan blijkbaar jaren duren voordat die foto wordt teruggestuurd. Kunnen jullie er een bovengrens in zetten? Zitten jullie onderdelen zo in elkaar dat jullie zeker weten dat de foto binnen 20 minuten of zo wordt opgestuurd?   +
Beweren en bewijzen/2014-15/feedback/voyager-deel2 +	* Ook hier klopt de natuurlijke taal niet. Jullie laten de foto naar de aarde sturen binnen 5 dagen dat het oorspronkelijke commando wordt verstuurd, maar de formule zeg (gelukkig) dat dat binnen 5 dagen na het maken van de foto is. Volgens mij hebben jullie namelijk nergens een beperking opgelegd over hoeveel u later is dan t. Dus misschien is de foto niet eens gemaakt binnen 5 dagen.   +
Beweren en bewijzen/2014-15/feedback/wasmachine-deel1 +	* De plaats van de exists is niet conform de systematische methode. * En verder is het natuurlijk bijzonder onrealistisch dat als jullie op tijdstip t het apparaat aanzetten dat op hetzelfde moment het viesWater beschikbaar is. * En wie weet wat de invulling van de u is? Ik zie geen enkel onderdeel dat me vertelt dat het ongeveer 68 minuten zal zijn of zo. * Ik zou verwachten dat er hier iets komt als: ** Als er op tijdstip t k kilo wasgoed in de trommel zit en er een programma p is gekozen waarvoor geldt dat de duur van dat programma minstens de noodzakelijke duur heeft om k kilo was schoon te maken en gedurende de hele duur van dat programma is de deur dicht, is er stroom en staat de machine aan, dan is er een moment na t (afhankelijk van de duur van programma p) waarop de was schoon is. (Extra eisen/resultaten als aanwezigheid van wasmiddel, schoon water gedurende de eerste twee minuten en vies water gedurende de rest van het programma en zo heb ik hier nu niet genoemd maar zijn misschien wel van belang.) ** Natuurlijk mogen jullie mijn voorstel zelf versimpelen, maar zorg wel dat er intervallen bij betrokken blijven.   +
Beweren en bewijzen/2014-15/feedback/wasmachine-deel1-her +	* Hier eisen jullie wel dat er een heel interval aan voorwaarden wordt voldaan, maar jullie onderdelen hebben dat helemaal niet nodig.   +
Beweren en bewijzen/2014-15/feedback/wasmachine-deel2 +	* Waarom staat er in natuurlijke taal iets vaags als 'minstens de programmaduur', maar in de formule iets over programmaduur + 5? * Ook hier weer syntax die niet conform de grammatica is.   +
Beweren en bewijzen/2014-15/feedback/zonnepaneel-deel1 +	De formule „E = A * r * Cd/683000 * PR” betekent volgens mij: De SiP- en SiB-lagen samen zetten 15% van de zonne-energie om in elektrische spanning, en de omvormer zet dat met 0,25 verlies om in wisselspanning. Overigens berekenen jullie niet de energie, maar het vermogen P. (De formule op de genoemde website berekent de energie per jaar, dat is dus ook een soort vermogen.) De relevante grootte, die je in plaats van Cd moet gebruiken, is de verlichtingssterkte, dat is de op een oppervlak invallende lichtstroom per oppervlakte-eenheid. (Wel komt het getal 683 terug: “a lumen represents ... 1/683 watts of visible light power” volgens http://en.wikipedia.org/wiki/Lumen_%28unit%29 ). De specificatie van het geheel die jullie daarna opgeven heeft echter niets te maken met die formule.  +