From leavens@cs.iastate.edu Tue Jan 22 21:31:12 2002 Date: Tue, 27 Nov 2001 19:10:03 -0600 From: Gary T. Leavens To: grads@cs.iastate.edu Subject: Please register for Com S 641 for Spring 2002 Hi, In Com S 641 (Semantics of Programming Languages) this coming semester, we will focus on an exciting and resurgent area of research in programming languages: techniques for formally deriving correct programs from specifications. In particular, we will explore a form of "wide-spectrum" programming language that includes specifications as statements in the language: the refinement calculus of Back and von Wright. The idea behind the refinement calculus is that one can write an "obviously correct" high level specification and then refine it in small steps into a correct and efficient implementation. Each refinement step has been previously justifed, and thus one constructs a proof of correctness along with the implementation. Besides the practial advantages, the refinement calculus is of considerable theoretical interest as a way of describing the semantics (meanings) of programming languages. It has been used with great effect to describe languages with callbacks, interactive concurrency, and other forms of parallelism. We will try to extend it to better treatments of object-oriented langauges, by adapting and extending the Java Modeling Langauge (JML) with refinement calculus features and using the theory to give a precise semantics to JML. JML is a language several of us at Iowa State are developing, and I'm excited about exploring its semantics and connections with the refinement calculus with you. The course will be small and there will be ample opportunity for interaction. The prerequisites for 641 are technically Com S 531 and Com S 541. If you don't meet these prerequisites and would like to take the class anyway, please see me and we can discusss it. Some details on past offering of Com S 641 (Semantics of Programming Languages) are found at the URL: http://www.cs.iastate.edu/~leavens/ComS641.html I hope to update this soon, but currently it only describes the old offerings. The course is listed with meeting times "to be arranged". I will arrange the schedule to suit the students in the class, so don't worry about schedule conflicts. (If you do sign up for the course, please send me your time schedule when it is finalized for the semester.) I'm happy to answer any questions you might have about the course also. Stop by to see me or send me an email if you have questions. Thanks, -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580