CSC501 Homepage

Programming Language Semantics

Fall 2011

Instructor:

Dr. Lutz Hamel
Tyler Hall Rm 251
Office hours: Mon and Wed 10am-11am and by apointment
email: hamel@cs.uri.edu

Description:

As processors become faster and computers become more interconnected our software systems become more complex to take advantage of these additional computational resources. This trend is also reflected in our programming languages where new features are evolving to deal with the distributed nature of our computational resources and to deal with the architecture of modern processors (e.g. multi-core processors). With this added complexity it is often difficult to establish that a program or programming language system behaves correctly. One way to approach the correctness of programs and language systems is to use formal methods. In this approach we usually construct a model of the software system or programming language system in a rigorous mathematical formalisms such as first-order logic and then prove that the model exhibits the intended (correct) behavior.

The application of formal methods applied to programming languages has two interesting points:

The latter is interesting in its own right from a language design perspective; once we have a formal description of every feature of a programming language we can study how features interact in a rigorous way; we can study if a particular feature has the intended behavior under special circumstances. Furthermore, we can achieve this without having to go through the trouble of building an actual implementation of the language. Thus, besides being able to establish correctness of software systems, in the case of programming languages formal methods are also a good design tool.

Formal methods applied to programming languages come in many different flavors under many different names such as "axiomatic semantics", "operational semantics", "denotational semantics", etc. each name indicating a different mathematical formalisms used to model a programming language. Collectively the approach of applying formal methods to programming languages is referred to as programming language semantics.

In this course we will use two flavors of first-order logic as our formal systems. The first approach uses first-order logic in conjunction with a deduction system called natural deduction and is usually referred to as natural semantics. The second approach uses a specialized version of first-order logic called Horn Clause Logic together with a deduction system called the resolution principle. The advantage of this latter approach is that the deductions in this logic are machine executable. Being able to execute deductions mechanically allows us to complete much more complex proofs than otherwise possible since the machine will handle many of the proof details. This approach is often referred to a executable operational semantics.

The aim of this course is to familiarize you with the basic techniques of applying formal methods to programming languages. This includes constructing models for programming languages and use these models to prove properties such as correctness and equivalence of programs. We will look at all major programming language constructs including assignments, loops, type systems, and procedure calls together with their models. Since many of our models are executable, we can test and prove properties of non-trivial programs.

Announcements:

[12/15/11] NOTE: the program in final in problem 3 (a) part 2 should read: 
[[defun,fact,[i],[if,[eq,i,1],1,[mult,i,[fact,[sub,i,1]]]]],[defvar,x,[fact,3]]]
[12/14/11] Posted solutions for assignment #6
[12/7/11] ** Final exam is due on Wednesday 12/21/11 @ noon in my office**
[12/7/11] posted the correctness proofs of loops and functions (see specs)
[12/2/11] Posted homework assignment #6
[11/23/11] Posted midterm solutions.
[11/22/11] Please bring your laptops to class today...we will be doing some correctness proof exercises.
[11/10/11] This time posted the correct version of the the solutions to assignment #5
[11/7/11] Posted solutions to assignment #5
[11/6/11] The midterm is now available. It is due in class on Tuesday 11/15/11.
[11/1/11] Hint for Assignment #5: when constructing proofs be careful about the kind of values you are looking at, most likely they are not values per se but structures that represent values, e.g. 
?- ['sem.pl'].
%   xis.pl compiled 0.00 sec, 7,792 bytes
%  preamble.pl compiled 0.01 sec, 8,920 bytes
%  xis.pl compiled 0.00 sec, 148 bytes
% sem.pl compiled 0.01 sec, 15,232 bytes
true.

?- asserta(lookup(x,s,vx)).
true.

?- (eq(x,x),s) -->> V.
V = (vx=:=vx).

?-
This is still a valid statement because the structure vx=:=vx represents an actual value. [10/27/11] Posted assignment #5
[10/20/11] Posted solution for assignment #4
[10/20/11] Posted the prolog specifications, see the specs folder
[10/13/11] posted assignment #4
[10/11/11] posted solutions for assignment #3
[10/5/11] posted assignment #3
[10/5/11] posted solutions for assignment #2
[9/30/11] solutions page is now live
[9/27/11] posted assignment #2
[9/22/11] the online gradebook website is live...email me for the access code if you haven't done so
[9/19/11] posted assignment #1
[9/7/11] You should go to the online grade book and sign up for an account (email me for your access code).
[9/7/11] Welcome!

Documents of Interest:

Literature Pointers


NOTE: email submissions are not acceptable for assignments.

Assignments: