Z/Larch Course

I see from Janet Wing's Larch survey that a number of you are
using Larch in undergraduate CS courses. 

For the past three years I've taught a second year CS undergraduate
course on formal notation and specification (using the Z notation).
Pretty simple stuff gets covered (models; representing data; schema
calculus; preconditions and elementary refinement).  At this level,
they seem to appreciate specification more when they also get to
see/develop actual concrete implementations. 

I'm currently considering how I can better teach students to be
precise(formal, when necessary) in the way they approach the
development of systems.  For next year's course, I've been seriously
thinking about `replacing' Z by Larch (lsl and lcl), so that students
can better experience (given the time provided) problem solving from
formal specification down to actual code.  Such a change, would to an
extent, result in my changing the general emphasis in the course to one
of a `reasoned approach' to programming/development.  But for second 
year students, this is probably a good thing.

I guess my main attraction to using Larch for teaching is: its
simplicity; its `obvious' connection with the programming process, 
and its useful tools.

I'd be grateful if any of you out there would relate your own
experiences of using Larch when teaching formal `methods'.

Would you reply/CC directly to me---I'm not yet on "larch-interest"
(waiting to see the results of the vote for Comp.specification.larch:-).


Simon Foley
Simon Foley,                         Email: simon@security.ucc.ie
Department of Computer Science,                 s.foley@cs.ucc.ie
University College,                  phone: +353 21 902929
Cork, Ireland                        fax:   +353 21 274390