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/2012-13/feedback/Dubbele schuifdeur-deel2 +	Dank je wel voor de tussenkopjes die jullie na de deadline hebben toegevoegd; dan zie ik de grote lijn in het bewijs.  +
Beweren en bewijzen/2012-13/feedback/Dubbele schuifdeur-deel2-her +	Het is al op 20 juni gelukt; daarover had ik al een opmerking gemaakt in mijn vorige beoordeling. Dank je wel voor de tussenkopjes.  +
Beweren en bewijzen/2012-13/feedback/Eukaryoot-deel2 +	Jullie beginnen heel raar met een exi_e op wat je moet bewijzen, terwijl die regel eigenlijk alleen zin heeft op exists uit de aannames. Na een stap of tien waarbij jullie ook nog eens een assumption over het hoofd zien zijn jullie weer terug bij af. En vervolgens doen jullie weer zo iets raars met een imp_e gevolgd door een imp_i. Een legale truc om iets met intervallen te kunnen bewijzen, maar op een 'normaal' moment in het bewijs zeer ongebruikelijk. En ook overbodig want asl jullie dit niet doen en gewoon verder gaan met 'fold GolgiApparaat' kunnen jullie het hele bewijs afmaken en hoeven jullie alleen aan het eind nog een paar lin_solve's toe te voegen.  +
Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel2 +	het was wel fijn geweest als er meer aandacht was geschonken aan de layout van de formules in het Coq-script. Ze zijn vaak breder dan de linkerkolom en toch niet verdeeld over meerdere regels. Positief is dat jullie lemma's definiëren en gebruiken. Echter, bij die lemma's gebeurt ook iets raars. Er staat een forall o:O in de formule terwijl er helemaal niets met o gedaan wordt. De enige reden dat dit gedaan wordt is denk ik omdat de specificatie van in dit geval Sensor niet volgens de systematische methode is gedaan, waardoor er een forall o:O over de hele conjunctie staat terwijl die alleen voor de eerste twee eigenschappen van belang is. Dit heeft tot gevolg dat jullie op een gegeven moment de eigenschap 'O' moeten bewijzen. Dat kan dan toevallig via assumption, maar wat betekent het dat jullie 'O' moeten bewijzen? Gebruikte regels: dis_e, dis_i1, dis_i2, apply, imp_e, imp_i, con_i, con_e1, con_e2, replace, lin_solve, interval, all_e, all_i.  +
Beweren en bewijzen/2012-13/feedback/Frisdrankautomaat-deel2 +	Bewijs werkt prima. Gebruikte regels onder meer exi_e, exi_i, lin_solve, replace. Er is gebruik gemaakt van Axiom, maar dat was met mijn toestemming.  +
Beweren en bewijzen/2012-13/feedback/Halon-Systeem-deel2-her +	ontbreekt geheel  +
Beweren en bewijzen/2012-13/feedback/Koelkast-deel2 +	Jammer dat er zo ruim wordt ingesprongen dat de formules niet meer in de linkerkolom passen. Het is erg onoverzichtelijk om unfold op alle onderdelen te gebruiken in plaats van alleen op het onderdeel waar het van belang is. Ook is de specificatie van het geheel hier weer anders weergegeven dan in het werkstuk zelf, maar nog steeds niet volgens de structuur van de formule. In het Coq-script wordt gewoon een conjunctie gesuggereerd, maar dat is het volgens mij niet. Gebruikte regels: neg_i, imp_e, imp_i, con_i, con_e1, con_e2, interval, lin_solve. Hiervan is alleen die neg_i een beetje bijzonder.  +
Beweren en bewijzen/2012-13/feedback/Koffiezetapparaat-deel2 +	Enkele van de eerder genoemde haakjes staan hier opeens wel... Jullie gebruiken de tactiek 'intuition', maar welke bewijsregels horen daarbij? fold en unfold van KoffieBak in H4, maar die staat in H3... Voor Coq maakt het niet uit, maar het ziet er wel wat onverzorgd uit. Verder doen jullie de exi_e's nu voor elke knop apart. Maar waarom niet in het begin gedaan voor dat de keuze van de knop gemaakt is? Dat zou ook conform de bewijsstrategie zijn. Jullie gebruiken Inductive om de eindige verzameling te maken, maar doen daar vervolgens niets mee. Nu hadden jullie een concrete invulling van muntwaarde kunnen maken door m100 op 100 te mappen en zo. In plaats daarvan gebruiken jullie gewoon de abstracte muntwaarde. Gebruikte (opvallende) regels: intuition, exi_e, exi_i, replace, lin_solve. Geen interval nodig gehad.  +
Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel2 +	onaf. Je legt de vinger precies bij het ontbrekende punt. Je zou namelijk aan de specificatie van het Stof_Reservoir zoiets moeten toevoegen als: Als de stofzak niet geleegd wordt, dan wordt de teller niet gereset.  +
Beweren en bewijzen/2012-13/feedback/Lift-deel2 +	Het bewijs werkt. De formules zijn netjes weergegeven in het Coq-script. Er wordt op een goede manier met het sub-artefact gewerkt. Dat is allemaal positief, maar... het bewijs is nogal simpel. Jullie gebruiken alleen de simpele regels imp_i, imp_e, all_e, con_i, con_e1 en con_e2. Zelfs geen all_i, want op die plaatsen hebben jullie gewoon imp_i gebruikt. Door (wat mij betreft) een fout in Coq wordt zo'n regel als all_i geinterpreteerd, waardoor het bewijs wel lukt, maar technisch gesproken is dit gewoon een foute toepassing van de regels.  +
Beweren en bewijzen/2012-13/feedback/Magnetron-deel1-her +	Jullie hebben in elk geval een Coq scipt toegevoegd, maar dat past helemaal niet bij jullie werkstuk. En in het bijzonder zitten er syntaxfouten in! Persoonlijk vond ik de specs in het werkstuk zelf beter dan deze...  +
Beweren en bewijzen/2012-13/feedback/Magnetron-deel2-her +	Toen ik het had over het toepassen van Lemma's doelde ik op de manier zoals je bij 'reverse' hebt gedaan. Het was niet de bedoeling om een nieuwe tactiek aan te maken. Het eindresultaat is echter mooi; helaas weet ik niet welke bron je gebruikt hebt om deze tactiek zo te definiëren. Verder zou ik ook graag uitleg hebben gekregen over hoe die tactiek nu werkt. Misschien zit er wel iets illegaals in deze tactiek? (Is niet zo, maar ik had het wel leuk gevonden als jij dat had opgemerkt.) Het voordeel van zo'n lemma is dat je dat lemma eerst moet bewijzen. Maar hoe bewijs je dat deze tactiek alleen maar eerlijke stappen gebruikt?  +
Beweren en bewijzen/2012-13/feedback/Melkrobot-deel2 +	Het bewijs is niet af. En ik denk eerlijk gezegd dat het verkeerde haakje in Carrousel wel eens de reden kan zijn dat de stelling nu niet bewijsbaar is.  +
Beweren en bewijzen/2012-13/feedback/Melkrobot-deel2-her +	Er worden lekker veel exi_e regels toegepast. Verder is het commentaar erg handig om te zien waar jullie mee bezig zijn. Wat bij sommige niet helemaal voor de hand liggende exi_e-regels wel handig is. Ook slim is de truc om eenmalig alle tijdsrelaties als expliciete aannames op te schrijven, zodat daarna de lin_solve-regels probleemloos werken.  +
Beweren en bewijzen/2012-13/feedback/Oven-deel2 +	De opmaak van de formules in het Coq-script is helaas slordig en voldoet niet aan de kwaliteitscriteria. En bij de Temperatuurdraaiknop staat in het Coq-script ineens een \/ daar waar er in de onderdeelspecificatie een /\ staat. Dat maakt nogal wat uit... Het is trouwens helemaal een andere specificatie geworden zie ik. Jullie bewijs is wel behoorlijk ingewikkeld. Jullie gebruiken onder meer neg_e', neg_i, lin_solve, interval, exi_e, exi_i, dis_e.  +
Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel2 +	Prettig dat er wat commentaar tussen staat waardoor beter te volgen is wat er op dat moment bewezen wordt. Gebruikte regels: exi_e, exi_i, dis_i1, replace, lin_solve, interval.  +
Beweren en bewijzen/2012-13/feedback/Stoplicht-deel2 +	onaf. Onvoldoende. In de laatste tak moet je iets bewijzen o.a. op basis van aanname H32b. Dat bewijs verloopt vrijwel precies zoals het bewijs op basis van aanname H32a. Coq is niet alleen magie. Ik verzoek je te proberen om te begrijpen wat je moet bewijzen: Er bestaat een tijdstip w in (v-20, v-8) waarop knop2 is ingedrukt, en je moet bewijzen dat één van de lichten voor auto’s op tijdstip v rood staat. Dat is echt bijna de situatie van aanname H32a (het enige verschil is dat daar knop1 was ingedrukt). Dan bedenk je eerst via welke onderdelen het bewijs verloopt en merk je dat H20 helemaal niet gebruikt wordt, dus dat dis_e overbodig is.  +
Beweren en bewijzen/2012-13/feedback/Stoplicht-deel2-her +	Ik bedenk achteraf dat je een deel van de herhalingen in een Lemma had kunnen stoppen, dat je één keer bewijst en dan meerdere keren met „apply <lemmanaam>.” aanroept, maar dat ik jullie niet eerder hierop heb gewezen kan ik jullie niet kwalijk nemen. In sommige delen is het ook alleen ''bijna'' een herhaling.  +
Beweren en bewijzen/2012-13/feedback/stofzuiger-deel2-her +	Alles in orde, dank je wel voor de commentaren die laten zien dat je niet alleen magie bedrijft.  +
Beweren en bewijzen/2012-13/feedback/verwarmingsysteem-deel2 +	onnodig ingewikkeld: „isI s0 /\ ingT s0 > kamerT s0” bewijs je door con_i. en daarna con_e1 (ingT s0 > kamerT s0). te doen, dus heen en terug naar dezelfde formule?  +
Beweren en bewijzen/2012-13/feedback/vriezer-deel2 +	Het bewijs werkt en is niet lang, maar alle elementen zijn er, zodat ik kan zien dat jullie het wel kunnen.  +
Beweren en bewijzen/2013-14/feedback/Carwash-deel2 +	Er zijn voldoende delen van het bewijs uitgewerkt, juist ook de interessante delen. In het niet-uitgewerkte deel zouden geen dingen aan bod komen die je nog niet kunt.  +
Beweren en bewijzen/2013-14/feedback/Cruisecontrol-deel2 +	Het bewijs is erg lang en gevarieerd. Overigens is het bewijs van de hoofdzakelijke correctheidsstelling te lang, bijna twee keer zo lang als nodig. Het belangrijkste verlengende element is dat je vaak een formule à la <tt>gasRatio (g1-1) (tijd1+1) /\ remRatio 0 (tijd1+1)</tt> bewijst met: con_i. con_e1 (remRatio 0 (tijd1+1)). ''( lang bewijs van'' gasRatio (g1-1) (tijd1+1) /\ remRatio 0 (tijd1+1) '')'' con_e2 (gasRatio (g1-1) (tijd1+1)). ''( nogmaals precies hetzelfde lange bewijs van'' gasRatio (g1-1) (tijd1+1) /\ remRatio 0 (tijd1+1) '')'' Elders moet je een tak bewijzen met de aannames <tt>tweeSecondenRegel v1 s1</tt> én <tt>~tweeSecondenRegel v1 s1</tt>. Pas nadat je bijna alles bewezen hebt zonder die tegenspraak te gebruiken, kom je erachter dat een bewijs met <tt>neg_e</tt> heel kort is.  +
Beweren en bewijzen/2013-14/feedback/De Game-deel1-her +	Een type zoals P kun je het beste definiëren met <tt>Inductive P: Set := speler | npc.</tt> Dan worden ook de constanten <tt>speler</tt> en <tt>npc</tt> gedefiniëerd. Ongeveer zoiets schreef ik ook al bij de eerste beoordeling.  +
Beweren en bewijzen/2013-14/feedback/NS in- uitcheck paal-deel2 +	De specificatie van het geheel is tamelijk eenvoudig, en in het bewijs maak je ook nog gebruik van flauwe hypothesen. Het zou kunnen dat bepaalde hypothesen nodig zijn, maar in ieder geval is hypothese <tt>berekenSaldo</tt> veel te sterk: elk nieuw saldo is acceptabel. Moet er niet tenminste een relatie zijn tussen oud saldo, kosten van de reis en het nieuwe saldo? Ook met hypothese <tt>genoegSaldo</tt> laat je een kans liggen om het bewijs interessanter te maken door soms een foutmelding te genereren.  +