Op eigenschap zoeken
Deze pagina biedt een eenvoudige bladerinteractie voor het vinden van entiteiten met een eigenschap met een bepaalde waarde. Andere beschikbare zoekinteracties zijn de zoekpagina voor pagina-eigenschappen en de querybouwer.
Lijst van resultaten
- Beweren en bewijzen/2014-15/feedback/PizzaAutomaat-deel2 + (
* Jullie gebruiken hier het interne fenom … * 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.moedelijk net in het bewijs weer goed komt. )
- 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/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/Lift-deel1 + (
* Jullie weten blijkbaar niet het verschi … * 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.geheel met de juiste parameters aan elkaar. )
- Beweren en bewijzen/2014-15/feedback/Airconditioner-deel2 + (
* Layout: de en-tekens en het pijltje kun … * 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.formule staat volgens mij heel iets anders. )
- 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/domotica-systeem-deel1-her + ( * Nog steeds lijkt alles op moment t te gebeuren. )
- Beweren en bewijzen/2014-15/feedback/Gene gun-deel1 + (
* Ogenschijnlijk ziet het er als een goed … * 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.de probleem bij de vacuükamer denk ik. )
- Beweren en bewijzen/2014-15/feedback/Eierkoker-deel1 + (
* Ook dit ziet er verdacht uit. De scope … * 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?ik alleen maar iets over 360 seconden zie? )
- Beweren en bewijzen/2014-15/feedback/voyager-deel2 + (
* Ook hier klopt de natuurlijke taal niet … * 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.s de foto niet eens gemaakt binnen 5 dagen. )
- 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/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/Helikopter-deel2 + ( * Originele eigenschap. Goede uitleg hierover bij conclusie. )
- Beweren en bewijzen/2014-15/feedback/Alarm-deel1 + (
* Probeer in het definitieve werkstuk erv … * 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.len bedoelen. Dat maakt het beter leesbaar. )
- Beweren en bewijzen/2014-15/feedback/Autowasstraat-deel2 + (
* Technisch gesproken is hij wel goed, ma … * 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.t je ook een exi_e gebruiken in het bewijs. )
- Beweren en bewijzen/2014-15/feedback/Pinautomaat-deel1 + (
* Tikfout in de namen van de predikaten.
… * 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.t jullie deze dubbele pijl kunnen bewijzen. )
- Beweren en bewijzen/2014-15/feedback/zonnepaneel-deel2 + ( * VO moet VC zijn? Of andersom? )
- Beweren en bewijzen/2014-15/feedback/stoplichten bij x-kruispunt-deel1 + (
* Waar is de natuurlijke taal?
* In de Fo … * 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?e richtingen. Wanneer krijgt hij dan groen? )
- 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/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/koffieautomaat-deel1-her + (
* Wat is de scope van die exists t2? Nu g … * 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.r ergens een 'niet' mist. Of te veel staat. )
- 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/Elektronisch deurslot-deel1 + (
* [ ] Ik snap het niet helemaal. Als ik d … * [ ] 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.cenario's uitprogrammeren als specificatie. )
- Beweren en bewijzen/2014-15/feedback/voyager-deel1 + (
* exists t:T gevolgd door een pijl? Julli … * 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?o binnen 20 minuten of zo wordt opgestuurd? )
- Beweren en bewijzen/2011-12/feedback/frituurpan-deel1 + (Afgezien van wat tikfouten ziet dit er hee … 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.gebruiken, maar dat doen jullie toch niet.)
- Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel2 + (Al ziet hij er wel een beetje verdacht uit.)
- 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/2011-12/feedback/xbox360-deel1 + (Alles lijkt op hetzelfde moment te gebeure … 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.u doet en wat er als resultaat te zien is.)
- Beweren en bewijzen/2012-13/feedback/Frisdrankautomaat-deel2 + (Behalve dan de layout van de formule.)
- 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/luchtontvochtiger-deel1 + (Bij de specificatie van het geheel gaat he … 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.gens hetzelfde soort fouten als in de CPU.)
- Beweren en bewijzen/2011-12/feedback/cylinderslot-deel1 + (Bij de specificatie van het geheel horen e … 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).t slot ook echt open gaat (of juist niet).)
- Beweren en bewijzen/2012-13/feedback/Melkrobot-deel1-her + (Davids toevoeging in natuurlijke taal in d … 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.ngen in de onderdelen te worden verbeterd.)
- Beweren en bewijzen/2014-15/feedback/Printer-deel1 + (De disjuncties moeten conjuncties worden. … 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”.ginnen met „voor al het papier ... geldt”.)
- Beweren en bewijzen/2012-13/feedback/Oven-deel2 + (De eerste helft van de specificatie van he … 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.l-entities die leesbaar zijn in de afdruk.)
- 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/2013-14/feedback/hdd-deel1-her + (De formule is geen vertaling van de zin in … 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.gData”. Dat mag niet. Verbeter dat alsnog.)
- Beweren en bewijzen/2013-14/feedback/boormachine-deel2 + (De formule is hier verbeterd, maar wederom … 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.net even iets groter kan zijn dan bedoeld.)
- Beweren en bewijzen/2014-15/feedback/zonnepaneel-deel1 + (De formule „E = A * r * Cd/683000 * PR” be … 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.eft echter niets te maken met die formule.)
- Beweren en bewijzen/2013-14/feedback/De Game-deel1-her + (De kwantor <tt>∃ k:K,</tt> lij … De kwantor ∃ k:K, lijkt me geheel overbodig omdat je de variabele k nergens meer gebruikt. Ook hier haakjes toevoegen: Signaal t (svk (Ctrl_knop_invoer t)). Signaal, toon_winst en toon_verlies zijn daarnaast geen invoer van het systeem als geheel, volgens het functionele netwerk. Dit schreef ik ook al bij de eerste beoordeling.an het systeem als geheel, volgens het functionele netwerk. Dit schreef ik ook al bij de eerste beoordeling.)
- Beweren en bewijzen/2013-14/feedback/Carwash-deel1 + (De laatste kwantor „&exists; t2:T,” is … 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.”taat een geldbedrag dat het juiste is.”)
- Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel2 + (De natuurlijke taal is niet zo heel erg na … 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.op een rare manier in de natuurlijke taal.)
- 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/2012-13/feedback/Scheerapparaat-deel1 + (De plaatsing van de ∀ x is heel raar. Er s … 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...eren' hierbij handig zijn...)
- Beweren en bewijzen/2012-13/feedback/Eukaryoot-deel2 + (De plaatsing van de kwantoren is wel raar. … 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?k in het verleden (voor t) aanwezig waren?)
- Beweren en bewijzen/2011-12/feedback/Printer-deel1 + (De samenhang van invoer en resultaat is niet gespecificeerd.)
- Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel1-her + (De specificatie in natuurlijke taal ontbre … 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?r is? Of wat betekent die /\ daar vooraan?)
- 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/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/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/2012-13/feedback/verwarmingsysteem-deel1 + (De specificatie moet zijn: Als de ingestel … 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.en hoe snel) de kamertemperatuur toeneemt.)
