Re: [isabelle] A course based on Isabelle/HOL and some feedback...
Thank you for the good resource.
Indeed, I am using the material to teach myself Isabelle. The material is
However, I found that myself cannot solve an exercise:
Prove a property of the %-calculus: % x. f x = % y. f y
which looks trivial, but whatever I try to make a lemma, they make syntax
Can anybody guide me?
On Thu, Apr 26, 2012 at 11:14 PM, Thomas Genet <thomas.genet at irisa.fr>wrote:
> 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
> The page of this course is here:
> 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
> ++ 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"
> 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 Genet
> 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 <http://www.irisa.fr/celtique/genet>
Charlie (Cheolgi) Kim
Visiting Research Scientist,
Real-Time System Integration Group,
University of Illinois
This archive was generated by a fusion of
Pipermail (Mailman edition) and