[Prev][Next][Index]
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:-).
Thanks!
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
--------------------------------------------------------------------