*To*: Thomas Genet <thomas.genet at irisa.fr>*Subject*: Re: [isabelle] A course based on Isabelle/HOL and some feedback...*From*: "Charlie (Cheolgi) Kim" <cheolgi at gmail.com>*Date*: Mon, 21 May 2012 14:38:13 +0900*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4F99585C.5090003@irisa.fr>*References*: <4F99585C.5090003@irisa.fr>

Thank you for the good resource. Indeed, I am using the material to teach myself Isabelle. The material is awesome. 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 errors. Can anybody guide me? Thank you. Best, Charlie Kim 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 > finders. > > The page of this course is here: > > http://www.irisa.fr/celtique/**genet/ACF/<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 <http://www.irisa.fr/celtique/genet> > > -- Charlie (Cheolgi) Kim Visiting Research Scientist, Real-Time System Integration Group, University of Illinois

**Follow-Ups**:**Re: [isabelle] A course based on Isabelle/HOL and some feedback...***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] isabelle2012-rc3\isabelle.exe removed by Norton when executed
- Next by Date: Re: [isabelle] Display Draft in Jedit
- Previous by Thread: Re: [isabelle] $HOME, $USER_HOME, and how I call "bin/isabelle" commands with batch/bash files
- Next by Thread: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list