Re: [isabelle] A course based on Isabelle/HOL and some feedback...
Le 26/04/12 17:23, Lukas Bulwahn a écrit :
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?
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
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.
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and