Re: [isabelle] A course based on Isabelle/HOL and some feedback...





Dear all,


Le 26/04/12 17:23, Lukas Bulwahn a écrit :
Hello Thomas,

I am impressed that simply writing and validating specifications with
Nitpick and Quickcheck could improve the correctness of the
implementations by 45%.
As you write, only 5% of the students got the right solution without
Isabelle in the beginning of the course, and 50% students ended up with
the correct program within 2 hours using Isabelle at midterm.

If you look at the predicate I was asking for it was not that complex to write in Isabelle/HOL (I realize that the subject of the lab is in french... sorry, I can translate it in french if you want to try)... I mean it is not straightforward but it only consists of 2 recursive functions... However, I think that coming up with the good solution at the first try is difficult.



Can you say more why 45% succeeded at midterm? Was it simply the
application of our counterexample generators and forcing students to
think about their specification?

Yes!

Why did the remaining 50% fail? Did they never get the specifications
right? Or did Quickcheck and Nitpick fail to find counterexamples?

No they had a hard time finding the good algorithmic idea and they are also beginners in functional programming... it is thus hard for them in 2 hours.


Further Isabelle tools adressing the problems of the remaining 50% might
be interesting to consider in the future.

except a tool automatically writing the functions from the specification ... I do not see how to help them :-) They were only lacking practice of functional programming. At the end of the course, they were more comfortable with this.

Best regards,

Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.