Eigenschap:Bewijscommentaar

Dit is een eigenschap van type Tekst.

Pagina's die de eigenschap "Bewijscommentaar" 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-deel2 +	Ontbreekt geheel.  +
Beweren en bewijzen/2011-12/feedback/ATB-deel2-her +	Het informele gedeelte van het werkstuk is in orde; het enige wat ontbrak was het bewijs. Maar helaas sluit ook het nu ingeleverde bewijs niet. Het eerste gat, waarin je correct een <tt>all_e</tt> wilt toepassen (uit <tt>forall t:T, TH t /\ ... -> SR (t+3000)</tt> concludeer je correct <tt>TH (t0-3000) /\ ... -> SR t0</tt>) kun je dichten met zoiets als <tt>replace t0 with (t0-3000+3000).</tt> Het tweede gat is een echt gat. Je moet niet alleen schrijven: „[I]k zie hier dat H[T]ehardRijden overeenkomt met de [conclusie]”, maar dat moet je met de bewijsregels die Coq aanbiedt '''bewijzen.''' Als je een paar stappen neemt, zie je namelijk dat HTeHardRijden <tt>HS t0 > MS t0</tt> bevat, maar dat de conclusie <tt>HS (t0-3000) > MS (t0-3000)</tt> eist. Waarschijnlijk moet je hier de specificaties van de onderdelen aanpassen zodat de zaak kloppend wordt. Bij het derde gat moet je eenvoudigweg de formule in delen opsplitsen (met <tt>con_i</tt>) en elk deel apart bewijzen. Om de formule in de juiste vorm te krijgen, moet je eerst <tt>exi_e (exists q:T, t0+3000<q /\ SS q /\ ...)</tt> gebruiken, en dat kun je eenvoudig bewijzen uit aanname HRemmer.  +
Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel2 +	Maar behoorlijk simpel. Jullie hebben welgeteld een keer een replace nodig, die vervolgens vrij eenvoudig te bewijzen is.  +
Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel2 +	omslachtig (maar niet incorrect) door herhaalde en overbodige invoering van dezelfde aanname.  +
Beweren en bewijzen/2011-12/feedback/Rekenmachine-deel2 +	Jullie leggen zelf uit waarom dit een prima proeve van bekwaamheid is.  +
Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel2-her +	alle stappen zijn formeel correct, alleen gebruik je op één punt de inconsistente aanname, namelijk bij <tt>con_e2 (v = (v - 12)).</tt> Omdat je kunt bewijzen dat <tt>v</tt> gelijk is aan <tt>v-12</tt>, kun je hier de moeilijkheden van het bewijs omzeilen. Ik zie uit de rest van het bewijs dat je wel serieus bezig bent.  +
Beweren en bewijzen/2011-12/feedback/airco-deel2 +	Het ingeleverde bewijs werkt niet. Ongeveer 40 regels voor het einde hangt hij met een syntax-error. En in de specificatie van het geheel staat hier opeens Lucht_binnen (t+6) terwijl het in de tekst hierboven nog gewoon t is. Dat past dan natuurlijk helemaal niet meer bij de natuurlijke taal. Wat wel goed is, is dat jullie een hulpstelling maken en die met apply gebruiken. Maar zorg dan svp wel voor wat tekst waardoor duidelijk wordt wat het doel is van die hulpstelling.  +
Beweren en bewijzen/2011-12/feedback/airco-deel2-her +	Jullie maken dezelfde fout als bij de vorige versie: er staat hier opeens een heel ander onderdeel dan bij de onderdeelspecificaties! Het onderdeel Bedieningspaneel is ineens een stuk ingewikkelder geworden. In het bijzonder mist hier uitleg in natuurlijke taal bij. Waarom is dit deel erbij gekomen? Welk onderdeel heeft deze eigenschap nodig?  +
Beweren en bewijzen/2011-12/feedback/cilinderslot-deel2-her +	Jammer dat die specificatie "de andere kant op" niet gelukt is te bewijzen. Was dat wel gelukt, was het cijfer echt hoger geweest.  +
Beweren en bewijzen/2011-12/feedback/cylinderslot-deel2 +	In het Coq-script worden opeens allerlei specifieke invullingen als profiel1 en profiel2 gegeven terwijl daar in het werkstuk zelf helemaal niets over gezegd is. Profiel1 gebruiken jullie nog wel in de definitie van profielSlot en in de definitie van sleutelPast. (Dat laatste is raar. Waarom staat daar niet de globale profielSlot? Als je nu met een ander slot gaat werken moet je op meerdere plekken iets gaan veranderen.) Maar de dingen als g1 en g2 zie ik nergens meer terugkomen. Het commentaar in het bewijs helpt wel om te zien waar we precies mee bezig zijn. In het bewijs doen jullie een unfold op SleutelPinnen, terwijl je iets bewijst met SluitPinnen. Technisch gaat dat goed omdat bij assumption Coq wel gaat zoeken of er een aanname is die past. Maar het staat wel slordig. Om dit te voorkomen zou je je bewijs niet met assumption, maar met exact moeten maken. Vervolgens openen jullie voor de volgende tak SluitPinnen terwijl jullie juist SleutelPinnen gebruiken. Verder maken jullie hier predikaten profielMatch, sleutelPast en juisteSleutelpinHoogte aan die eigenlijk helemaal geen predikaten zijn, maar hulpdefinities.  +
Beweren en bewijzen/2011-12/feedback/elektrische tandenborstel-deel2 +	Ik ben niet blij met de keuze om Coq de gebonden variabelen te hernoemen. Ik zie liever zinvollere namen als 'startmoment' of zo. Gelukkig hielp de naamgeving van de aannames vaak wel wat, al waren ze soms ook wat cryptisch. Goed gebruik gemaakt van de verschillende regels: interval, exi_e, neg_i en neg_e'. Hebben jullie nog geprobeerd om het zonder neg_e' te kunnen doen?  +
Beweren en bewijzen/2011-12/feedback/fiets-deel2 +	Wel weer goed dat jullie de gebruikte iff_e regels uitleggen.  +
Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel2 +	Zoals verwacht een tamelijk simpel bewijs. Er zit geloof ik een keer een replace in om de zes seconden tijdsverschil in een stuk van vijf en van een te hakken, maar dat is ook zo ongeveer het moeilijkste wat er in zit.  +
Beweren en bewijzen/2011-12/feedback/frituurpan-deel2 +	Waarom hebben jullie gekozen voor Z_scope? Op zich is het bewijs natuurlijk wel goed, maar er zit geen enkele moeilijke stap in. Geen replace, lin_solve, interval...  +
Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel2-her +	Tja, het bewijs is alleen maar rondgekregen doordat er gebruik gemaakt wordt van twee keer een hypothesis, waarbij elk van die aannames zeer discutabel zijn. Zeg maar gewoon fout. Ze hebben namelijk de vorm van de standaardfout dat ∀ gecombineerd wordt met ∧ tekens.  +
Beweren en bewijzen/2011-12/feedback/kassa-deel2 +	Prettig dat er met commentaar is aangegeven welke goal er bewezen moet worden. (Als stond er wel ergens een 0 in plaats van VTB (a + 7100 + 1000).) Zoals gezegd is het jammer dat jullie jullie bewijskwaliteiten niet helemaal tonen. Jullie hebben op een gegeven moment een ∃ in de aanname, maar omdat de intervallen precies overeenkomen, hoeven jullie die niet eens met de exi_e regel uit te werken om vervolgens te laten zien dat er echt zo'n moment is.  +
Beweren en bewijzen/2011-12/feedback/lift-deel2-her +	Het bewijs van KnopNaarWachtlijstStelling is fout. Er staat een foute typering in 'Logica t' en op diezelfde plek is vergeten eerst een all_e te doen alvorens Logica eraan te koppelen. Verder had ik graag toelichting gezien op de invulling van jullie functie Afstand. Die lijkt namelijk een kwadratische afstand weer te geven in plaats van de echte afstand. Nu wordt hij nooit echt gebruikt (via unfold), dus maakt het niet uit voor het bewijs. Ook gebruiken jullie hier een andere specificatie bij Bewegingsmechanisme: de ∃ is opeens een ∀ geworden! Tenslotte gebruiken jullie hier opeens een commando 'intros' dat niet behandeld is en ook niet door jullie uitgelegd wordt.  +
Beweren en bewijzen/2011-12/feedback/loopband-deel2 +	Op zich ziet het bewijs er prima uit. Veel noeste arbeid. Netjes uitgelegd hoe die iff_e en iff_i regels werken. Alleen wel jammer dat de inhoud van Resetten blijkbaar niet van belang is. Als je die vervangt door 't is ongelijk aan t', kan precies hetzelfde script gebruikt worden. Dus blijkbaar is het niet van belang of er achter Resetten iets zinnigs of onzinnigs zit.  +
Beweren en bewijzen/2011-12/feedback/magnetron-deel2 +	Het eerste dat opvalt is dat er in jullie domeinmodel een eindige verzameling vermogens wordt gegeven, terwijl jullie hier gewoon zeggen dat het de hele R is. Voor het bewijs maakt het blijkbaar niets uit dat jullie je in de tekst beperkt hebben tot drie standen, want dit bewijs werkt ook voor andere vermogens. Helemaal op het eind doen jullie iets raars in het bewijs: een imp_e (d1>0) gevolgd door een imp_i H. Maar de aanname d1>0 hadden jullie al. Deze stappen zijn dus overbodig. Misschien had het geholpen als jullie ook eens fold gebruiken om aannames die niet meer van belang zijn dicht te klappen. Dan wordt het een beetje overzichtelijker.  +
Beweren en bewijzen/2011-12/feedback/ov-oplader-deel2 +	Jullie hebben ervoor gekozen om de verzameling berichten abstract te houden met als enige kennis dat mChipkaartOpgeladen en mChipkaartIngevoerd variabelen van dat type zijn. Die kunnen dus nog wel het zelfde zijn. En er kunnen ook nog veel meer berichten zijn. Maar in jullie bewijs maakt het niet uit. Het positieve aan het bewijs is dat jullie zowel exi_e-regels als lin_solve-, replace- en interval-regels gebruiken. Jullie specificatie van het geheel wijkt dus genoeg af van de onderdelen om echt te kunnen laten zien dat er werk verzet moet worden.  +
Beweren en bewijzen/2011-12/feedback/waterkoker-deel2-her +	Qed ontbreekt, maar dat is natuurlijk niet echt essentieel.  +
Beweren en bewijzen/2012-13/feedback/Alarmsysteem-deel2 +	Het bewijs is duidelijk onaf; je hebt net iets meer gedaan dan de eerste triviale stappen. Bovendien voer je dis_i en dis_e in de verkeerde volgorde uit. „replace (b+30) with a.” is waarschijnlijk ook niet goed; je moet dan namelijk bewijzen dat b+30=a is, maar dat zal moeilijk lukken, omdat je beide als onbesproken variabele hebt geïntroduceerd.  +
Beweren en bewijzen/2012-13/feedback/Alarmsysteem-deel2-her +	Twee onmogelijk te bewijzen takken: *Zoals ik al drie keer heb aangegeven, zul je geen relatie tussen a en b (a=b+30 of b=a+30) kunnen bewijzen omdat je beide variabelen als onbesproken hebt geïntroduceerd. *Als de negatie van een existentiële uitspraak in de aannames staat, kun je normaliter niet bewijzen dat deze existentiële uitspraak waar is. De exi_e-regel is niet te bewijzen. Verdere onhandigheden: * Je splitst een formule met con_i op en voegt direct daarna met con_e1 het zojuist afgesplitste deel toe. Als resultaat moet je dat twee keer bewijzen i.p.v. één keer. * Als gevolg van die onmogelijke existentiële uitspraak (hierboven) voer je een neg_e-regel uit. Die regel moet je eigenlijk alleen uitvoeren als je al ziet dat er een tegenspraak in de '''aannames''' zit. Dat de conclusie de aannames tegenspreekt is misschien een hint, maar dan moet je op zoek naar de tegenspraak in de aannames.  +
Beweren en bewijzen/2012-13/feedback/Bankkluis-deel2-her +	Technisch gesproken goed, maar jullie hebben waarschijnlijk ook wel gemerkt dat jullie alleen de simpele regels imp_e, imp_i, all_e, all_i en zo nodig hebben gehad. Overigens is het wel handig om zinnige namen te geven. Nu gebruiken jullie t5 voor het moment waarop de code wordt ingetoets en t3 (een later moment) voor het moment waarop de sleutel wordt ingestoken. Dat is verre van logisch en verwarrend. Als jullie zinnige namen als 'tcode' of 'tsleutel' (of 'tc' en 'ts' als jullie die andere namen te lang vinden) zouden gebruiken, is het veel makkelijker te zien wat het allemaal voorstelt.  +
Beweren en bewijzen/2012-13/feedback/Draaideur-deel2 +	Het bewijs is van veel commentaar voorzien om met name het begin van structuur te voorzien. Naarmate het bewijs vordert wordt dat wel minder. Ook herkende ik nog wat van mij eigen commentaar... Niet-standaardregels: dis_e, exi_e, exi_i, interval, lin_solve. Replace niet nodig door goed gebruik van stappen als exi_i (t_pid + 8 + 1).  +