241
U
Eigenschap:Domeinmodelcommentaar
Uit Werkplaats
Dit is een eigenschap van type Tekst.
Pagina's die de eigenschap "Domeinmodelcommentaar" gebruiken
Er zijn 25 pagina's die deze eigenschappen gebruiken.
B | |
---|---|
Beweren en bewijzen/2011-12/feedback/ATB-deel1 + | Meet de snelheid in m/s of in km/h. Het predicaat TeSnel is ongelukkig uitgelegd: zoals het er staat is het overbodig (omdat het eenvoudig uit de functies HuidigeSnelheid en MaximumSnelheid gedefinieerd kan worden), maar op basis van de specificatie van de Vergelijker begrijp ik dat het eerder zoiets is als: De vergelijker geeft aan dat de trein te snel rijdt. HuidigeSnelheid en MaximumSnelheid zijn geen predicaten, maar functies, omdat hun resultaattype niet B is. Het predicaat Rem kan niets blokkeren; een predicaat beschrijft alleen bepaalde eigenschappen van onderdelen, b.v. dat de Remmer een signaal naar de remmen stuurt. De meting van Rem lijkt me niet helemaal te passen. + |
Beweren en bewijzen/2011-12/feedback/ATB-deel1-her + | Een detail: Als een naam al kort is, zoals Bel, hoef je niet een aparte afkorting te definiëren. + |
Beweren en bewijzen/2011-12/feedback/ATB-deel2 + | De meeste hulpdefinities zijn goed; alleen AfstandCorrect heeft een onnodig ingewikkelde definitie: als de trein stilstaat, is HS t = 0, dus hoef je geen ingewikkelde berekening uit te voeren om vast te stellen dat de remafstand = 0 is. + |
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel1 + | Het is erg vaag dat er 'een bepaalde intensiteit' wordt gemeten. Juist omdat jullie toch willen kijken wat er gebeurt afhankelijk van de sterkte van het licht, kunnen jullie beter een predikaat 'licht' maken met een extra parameter van type L. De betekenis geeft dan aan dat op tijdstip t er licht met intensiteit l wordt gedetecteerd. Zelfde probleem bij beweging. Ook is het heel raar dat in de betekenis van lamp_brandt opeens een t+30 staat. + |
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel1-her + | Er staan wel wat rare ronde haken bij jullie bereiken. Verder lijkt die 130000 wel erg hoog ten opzichte van de 10 die jullie als ondergrens zien. Hoe reeel zijn beide waarden? Ik ben geen expert, jullie wel, dus misschien kunnen jullie ergens (bij focus ofzo) een beetje uitleggen wat 130000 lux betekent? Is dat tegen de zon in kijken ofzo? Is 10 de waarde die met schemering overeenkomt? + |
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel2 + | Er staan nog steeds gekke ronde haken bij het bereik. In het bijzonder zit 0 dus niet in jullie verzameling L. Dat had ik de vorige keer toch al gemeld? Waarom hebben jullie hier allemaal functies gemaakt? Zijn dit eigenlijk niet gewoon predikaten met bijvoorbeeld als tweede parameter iets van type L? + |
Beweren en bewijzen/2011-12/feedback/Beertender-deel1 + | De kolom „afkortingen” is bedoeld voor het geval dat je zeer lange namen van predicaten of functies in formules en bewijzen wilt afkorten. Omdat je dat niet doet mag je de kolom leeg laten. + |
Beweren en bewijzen/2011-12/feedback/Beertender-deel2 + | Predicaat perfectBier vraagt een parameter die de bierhoeveelheid aangeeft, maar in de omschrijving van het predicaat zie ik niet wat die parameter voor functie heeft. + |
Beweren en bewijzen/2011-12/feedback/Blokfluit-deel1 + | Het domein van mensen is overbodig omdat je slechts over één fluitist en één luisteraar spreekt. (Je hoeft niet te modelleren dat verschillende mensen op verschillende manieren spelen.) In de kolom „type” moet je aangeven wat de invoer- en uitvoertypes van de functies en predicaten zijn, b.v. „F -> B” voor een predicaat dat een frequentie als parameter heeft en een boolean oplevert. Predicaten hebben altijd resultaattype B, functies altijd een ander resultaattype. + |
Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel1 + | Het predicaat Wa lijkt te ontbreken. (Als je de predicaten al met de korte naam definieert, hoef je ze niet apart als afkorting op te nemen.) De meting van „Er is rook” zou je met een onafhankelijk testinstrument kunnen testen, maar zoals het geformuleerd is lijkt het erop dat je de uitvoer van de rookmeter als meting beschouwt, en dan krijg je een cirkelredenering. + |
Beweren en bewijzen/2011-12/feedback/Printer-deel1 + | Er kan gespecificeerd worden dat er printactiviteit is. Maar niet dat er na verloop van tijd daadwerkelijk een geprint document ''ligt''. Waar het om aankomt is dat, ald men de interne codering d:D van een document stuurt, dat er een leespare representatie repr(d) zichtbaar op het papier staat. + |
Beweren en bewijzen/2011-12/feedback/Rekenmachine-deel1 + | HEt domeinmodel is niet onzinnig, maar jullie houden het meest interessante er buiten. Als je het spel zo wilt spelen, kom je uit met een een predicaat: "de uitvoer is juist voor de gegeven invoer", en dan wordt het triviaal. Wat je wilt kunnen specificeren is dat er twee getallen x en y ingetoetst worden, dat er een plus-knop gedrukt wordt, en dat een bepaald getal (laten we hopen x+y) verschijnt. De namen van de predicaten bevatten spaties, hetgeen niet kan in onze taal. Hoe vol een batterij is, wordt normaliter gemeten door haar spanning te meten. Voor een gegeven batterijsoort is daaruit de capaciteit af te leiden. Als je al een kwantitatief predicaat hebt, heb je batterij vo en batterij leeg niet als aparte predicaten in het domeinmodel nodig. + |
Beweren en bewijzen/2011-12/feedback/Roltrap-deel1 + | We willen dat de namen van predicaten in het domeinmodel gelijk zijn aan de namen van signalen die in het functioneel netwerk gebruikt worden; dan wordt de relatie tussen de twee duidelijker. Ik vermoed dat PNoordrem een tikfout voor PNoodrem is. + |
Beweren en bewijzen/2011-12/feedback/Segway-deel1 + | Het predikaat ''goed gewicht'' is niet nodig in het domeinmodel. Je kunt het DM kleiner maken door bij veel predikaten een parameter voor de zijde (links, rechts) toe te voegen. + |
Beweren en bewijzen/2011-12/feedback/Segway-deel2 + | Een aantal functies (vb, hs) hebben vreemde types en zijn inconsistent beschreven. De Coq-notatie wijkt daarvan af. Daar hebben deze functies een overbodige parameter. Al met al is niet duidelijk wat er bedoeld is. De conversiefuncties zijn niet als 'black box' gegeven maar uitgeprogrammeerd. Het is niet duidelijk of dit tot ongewenste effectel leidt. Waarom is 'goed gewicht' in natuurlijke taal gespecificeerd en niet in logica? + |
Beweren en bewijzen/2011-12/feedback/Vaatwasser-deel1 + | Waarom kies je ervoor om even_minuut als functie te behandelen? Het resultaattype is booleaans, net als bij predicaten. Geef het predicaat „knop_gedrukt” een duidelijkere naam: Welke knop is ingedrukt? (Terzijde: Een geiser, met s, is een doorloopverhitter voor kraanwater die meestal op gas gestookt wordt. Het onderdeel van de vaatwasser kun je misschien „verwarmingselement” of „waterverhitter” noemen.) + |
Beweren en bewijzen/2011-12/feedback/Vaatwasser-deel2 + | Het predicaat <tt>even_minuut</tt> kun je als een hulpdefinitie behandelen, omdat het gemakkelijk uitgerekend kan worden. (Overigens krijg je dat de vaatwasser het programma net iets anders afdraait als je hem in een oneven minuut start.) + |
Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel1 + | Het belangrijkste, de temperatuur, wordt niet meegenomen in het domeinmodel. + |
Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel2-her + | „s graden” bij huidigeTempSignaal, ingesteldeTemp en verwarmWater is niet helemaal exact, maar goed genoeg. De meting van radiatorWater lijkt me wat vreemd. Onduidelijk is of je tijd in seconden of minuten meet. Hulpdefinitie: teKoud geeft eigenlijk niet aan of de '''huidige''' temperatuur te laag is, maar of de '''gemeten''' temperatuur te laag is. + |
Beweren en bewijzen/2011-12/feedback/airco-deel1 + | Bij ControleUnitAlgoritme ontbreekt een parameter. Verder staan er in het netwerk enkele namen die niet in het domeinmodel staan, maar als hulpdefinitie. Dat is niet echt gebruikelijk, maar hier misschien wel handig. Overigens kan het geen kwaad om ook de hulpdefinities van uitleg in de vorm van natuurlijke taal te voorzien. En Tempratuur schrijf je anders... + |
Beweren en bewijzen/2011-12/feedback/airco-deel2 + | De betekenis van het controleunitalgoritme had natuurlijk niet in de tabel, maar bij de hulpdefinitie moeten staan. En in het bijzonder had er niet iets als 'schakelt hij aan' moeten staan. Hij schakelt niets. Hij levert een boolean op en heeft geen idee wat de andere onderdelen met die boolean doen. En een betekenis als 'op tijdstip t is er een signaal' zegt natuurlijk niets. Wat voor een signaal? Van waar naar waar? Een aan-signaal of juist een uit-signaal. Bij de vorige feedback heb ik gevraagd om uitleg in natuurlijke taal bij de hulpdefinities. Die staat er echter nog steeds niet. Ook had ik de vorige keer expliciet op een tikfout gewezen. Zelfs die is niet verbeterd. Hebben jullie de feedback wel gelezen? En wat stellen die constanten voor? Wat is tempGas voor een speciale temperatuur? + |
Beweren en bewijzen/2011-12/feedback/airco-deel2-her + | Duidelijk verbeterd ten opzichte van vorige versie. + |
Beweren en bewijzen/2011-12/feedback/cilinderslot-deel2-her + | Gebruikelijk is om de invulling van de hulppredikaten hier al expliciet te maken, zodat duidelijk is dat het echt hulppredikaten zijn die volledig te maken zijn met de al bestaande predikaten. Gelukkig komen ze uiteindelijk wel in het Coq-script. + |
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel1 + | De grootste fout is dat dit domeinmodel absoluut niet past bij het netwerk. Ik zie allemaal nieuwe namen. Daarnaast zijn er ook nogal wat technische opmerkingen te maken: * Die verzameling positieve integers, is dat een begrensde verzameling? En dus eindig? Het stellen immers de posities voor en als ik het goed gezien heb is dat in dit werkstuk momenteel alleen 1, 2 of 3. * Bij de betekenissen gebruiken jullie dezelfde hoofdletters H en L als bij de types. Maar in de betekenis gaat het juist om een element van zo'n H, een instantie dus. Die wordt traditiegetrouw in kleine letters geschreven. Het mooiste is om iets te schrijven als 'profielMatch p1 p2' betekent 'profiel p1 van de sleutel past bij profiel p2 van het slot'. Dan is tenminste ook meteen duidelijk welk argument nu over de sleutel gaat en welk over het slot. Met name is dit bij slutelPinVerplaatsing en sluitPinVerplaatsing onduidelijk. Daar staat een zin in gebrekkig Nederlands die niets zegt over de rol van de parameters. Ook bij sleutelInSlot staat een beetje onduidelijke betekenis. Zeg liever iets als ' sleutel k zit in het slot'. Wat ik hier bijzonder verdacht vind, is het feit dat er geen predikaat 'slot_open' is. Jullie willen bij de specificatie van het geheel toch zeker iets zeggen dat er soms wel en soms geen slot geopend is? Dan moet je daar wel een predikaat voor hebben. + |
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel1-her + | Vorige keer schreef ik: ''De grootste fout is dat dit domeinmodel absoluut niet past bij het netwerk. Ik zie allemaal nieuwe namen.'' Dat commentaar geldt nog steeds. De predikaten hier komen niet terug in het netwerk en de predikaten in het netwerk komen niet terug in het domeinmodel. Verder hebben jullie het commentaar over het gebruik van de parameters in de betekenissen op sommige plekken wel aangepast, maar op andere plekken niet. Ik zie nog steeds hoofdletters op plaatsen waar ik kleine letters verwacht en ik zie nog steeds betekenissen waar helemaal geen parameters worden genoemd. + |