Eigenschap:Specgeheelcommentaar

Dit is een eigenschap van type Tekst.

Pagina's die de eigenschap "Specgeheelcommentaar" gebruiken

Er zijn 25 pagina's die deze eigenschappen gebruiken.

(vorige 25 | volgende 25) (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.  +