From leavens Mon Aug 15 13:03:49 1994
Return-Path: <leavens>
Date: Fri, 11 Mar 94 11:45:40 CST
From: leavens (Gary Leavens)
To: grads@cs.iastate.edu
Cc: leavens, faculty@cs.iastate.edu
Subject: Please sign up for 641 in the Fall

	This is a preliminary announcement for Com S 641, which (I hope)
will be offered this Fall.  If you like(d) Com S 541 (programming langauges 1)
you will enjoy Com S 641.

	Com S 641 focuses on the semantics of programming languages.
This time I'd like to zero in on an approach we typically don't cover
in Com S 541: axiomatic semantics.  Axiomatic semantics is important
and useful because it relates directly to program specification/verification.
In axiomatic semantics, one specifies the meaning of programming language
constructs by giving a verification logic for the language.

	My plan is to use a recent monograph by Wim H. Hesselink
titled "Programs, Recursion, and Unbounded Choice" (Cambridge, 1992).
This monograph does a beautiful job of describing the latest thinking
in what Hesselink calls "transformational calculus semantics" and he handles
constructs such as while loops, recursive procedures, induction, and
nondeterminism.  The treatment is very thorough, and has the added bonus
of reflecting the latest thinking about program verfication.

	We will supplement the book with other papers as needed,
and will spend a bit of time at the beginning of the semester
explaining program verification and Dijkstra's calculational style of proof,
which Hesselink uses.  We will also try to apply these techniques
to object-oriented programming languages with subtyping and message passing.

	Thus this edition of Com S 641 should be of interest if
you are working in either specification, verification, or programming language
semantics.

	As you may know, a class like Com S 641 is typically small,
and allows a lot of interaction.  To make sure it isn't too small
(and thus canceled), please sign up for it when you register.
We'll arrange a meeting time convenient for all.

	Gary Leavens

P.S. If you're a faculty member advising students who could benefit from such
a class, please urge your students to sign up.