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




Dear all Isabelle users,


as promised to Tobias and Jasmin here is some feedback and teaching material for a course that I gave this year on Formal Analysis and Design to students in a first year of Master in computer science.

This course was designed for our "professional" master students i.e. that will end up developpers and not for "research" master students that will end up in PhD. Thus, I focused on functional programming (Isabelle/HOL and Scala), first order logic (for defining program properties) and on counterexample finding (rather than on proof). The final objective is to run Java+Scala programs with verified blocks, i.e. whose formally defined properties have been checked on the Isabelle theory using counterexample finders.

The page of this course is here:

http://www.irisa.fr/celtique/genet/ACF/


With regards to the experience the students had with Isabelle/HOL here are some comments. I already sent them to Tobias and Jasmin but Jasmin advised me to send them on the mailing list.



Good points:

++ Though 80% of the students were initially allergic to functional
   programming, in the end they are almost all convinced that it is
   a convenient formalism to define and prove programs.
+++ Students allergic to logic ended up in writing relevant lemmas
    (this point deserves three +, because it was my main objective)
++ Most of the students allergic to logic ended up in being convinced
   that writing a lemma may replace writing a test
++ Some of the students ended up in being convinced that writing a
   lemma may replace writing a thousand tests :-)
+++ Counterexample generation makes it possible for the students to
quickly figure out which of their definition (the lemma or the function) was
    false.
++ The code export to Scala was very much appreciated ... it makes the
formal verification of functional program sounding useful to developpers!
++ Counterexamples found by nitpick and quickcheck permitted to debug
   rather complex functions (see practicals in the following). They
   were intensively used by students.


Bad points and suggested improvements:

--- Function parser and error messages are sometimes very poor... which
    makes the debugging very difficult... especially for functions of more
    than 10 lines the error message just mention that there is an error
    somewhere... well, thanks :-)  At least, a line number for the error
    would be much appreciated.

-- It is a bad idea to use a variable name like id in a function
  equation, e.g.:

fun f:: "nat => nat"
where
"f(id)=id"

  OK, the error message says:
*** Type error in application: incompatible operand type
***
*** Operator:  f :: nat => nat
*** Operand:   id :: ??'a => ??'a

  and a (careful) student may understand that 'id' is already defined as a
  function etc... however this is far more difficult to find when the
  function has 10 complex equations. What surprises me is that the
  left-hand side of the equation f(id) does not respect the restrictions
  for "fun" declarations and that it should be rejected anyway (with a
  more explicit error message). Am I right?

- Indentation of function equations (inside the "...") is simply horrible (in emacs) as soon as you have several if and case constructions, or I did not understand it.



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.