CSC501 Homepage

Programming Language Semantics

Fall 2016

Instructor:

Dr. Lutz Hamel
Tyler Hall Rm 251
Office hours: Monday 11-noon Tyler 251, Wednesday 1-2pm Tyler 251, or by appointment
email: hamel@cs.uri.edu

Announcements:

[12/15/16] NOTE: there is a typo in the final. Question 3(b)1. should read [add,1,2].
[12/15/16] posted all solutions for csc501 including solutions to the EC midterm and assignment #6.
[12/12/16] *** final due Monday 12/19 in Sakai ***
[12/6/16] posted assignment #6 -- no late assignment accepted
[11/23/16] Here is an answer to the question with regards of specifications, proofs, and real machines that was posed earlier today in class. The question was, given the specification:
∀s,∃Q,V1,V2 [(p,s)−−≫Q ∧ lookup(z, s, V1) ∧ lookup(z, Q, V2) ∧ V2 = 2 ∗ V1]
If we want this to be valid on real machines then we will have to include information about the real machine in the proof. In this case we would have to specify integer overflow conditions. Consider the predicate 'valid_range(I)' that returns true if integer I is within the specified integer range of a particular machine otherwise it will return false. Now we can use this to make our proof water tight in the sense it will tell us under which conditions program according to the specification are no longer correct:
∀s,∃Q,V1,V2 [(p,s)−−≫Q ∧ lookup(z, s, V1) ∧ lookup(z, Q, V2) ∧ V2 = 2 ∗ V1 ∧ valid_range(V1) ∧ valid_range(V2)]
This can be written much more elegantly using pre and post conditions:
pre(R) = lookup(z,R,v1) ∧ valid_range(v1)
and the post condition:
post(Q) = lookup(z,Q,v2) ∧ v2 = 2*v1 ∧ valid_range(v2)
such that for a given program p we have,
∀s,z,∃Q[(p,s)-->>Q ∧ pre(s) ⇒ post(Q)]

[11/22/16] *** Extra credit for midterm available. Due Tuesday 11/29/16 in Sakai *** The extra credit calculation will be as follows:
final midterm grade = part I + max(part II, EC)
if you have submitted extra credit work.
[11/22/16] posted solutions for the midterm
[11/17/16] There is a typo in Part II problem 1(c) second program. It should read:
get seq 
duplicate seq 
pop(x) seq 
get seq 
duplicate seq 
pop(y) seq 
le seq 
if(
   (push(y) seq put),
   (push(x) seq put))
[11/16/16] Hints for the midterm, part II. Your semantic rules should look very similar to the rules given for the IMP language in class. Consider the stack machine command 'add'. This is syntax that needs to be interpreted in the context of a state. A state in our case is a pair consisting of a binding list and a stack. So the rule for add should look something like this:
(add, (List,[A,B|Stack])) -->> (List,[C|Stack]) :-
     int(A),
     int(B),
     C xis B + A,!.
Here I assume that the stack is implemented as a list.
[11/16/16] posted solution to assignment #5
[11/10/16] posted the midterm. Due Sunday 11/20/16 in Sakai
[11/4/16] posted assignment #5
[11/2/16] posted solutions for #4
[10/26/16] Posted assignment #4
[10/24/16] You should start reading this tutorial and install SWI Prolog...you will need it for the next homework!
[10/24/16] posted solutions for #3
[10/17/16] posted assignment #3
[10/14/16] posted solutions for #2
[10/7/16] for my proofs in Latex I use a package call bussproofs. Check out the link for any relevant documentation.
[10/7/16] posted assignment #2
[9/23/16] posted assignment #1 -- see below
[9/16/16] To clear up any confusion about 'iff' which is a shorthand for 'if and only if' let's take a closer look. This logical connective consists two implications the 'if' implication and the 'only if' implication. However, for non-native English speakers it is confusing which part of 'if and only if' represents an implication in which direction. We can write 'if and only if' as two separate statements. Let A and B be two assertions, then:
A iff B ≡ 
(A if B) ∧ (A only if B) ≡ 
(if B then A) ∧ (if A then B) ≡
B ⇒ A ∧ A ⇒ B ≡
A ⇔ B
So, given the expression A iff B, the thing to remember is that 'if' goes from right to left and the 'only if' goes from left to right.

[9/13/16] Some thoughts on P(P(∅)) where P is the powerset operator and ∅ denotes the empty set. Before we get there let's take a look at the definition of the natural numbers N, since I raised that issue in class. The natural numbers N are defined as the set,

N = {0,1,2,3,...}

with the additional structure that 0 < 1, 1 < 2, etc. Sets that have this additional kind of structure are referred to as posets (partially ordered sets).

Now, the question is: is there a deeper mathematical definition of the natural numbers beyond just defining digit symbols and defining an order among the digit symbols? The answer is YES! We can define a mathematical meaning for the digit symbols in terms of sets and what is most interesting is that the ordering among the natural numbers is contained within this definition.

Consider the set ∅. The cardinality of this set is 0,

#∅ = 0

Now consider the successor function s,

s(∅) = {∅}

Note that #{∅} = 1. That is, the successor of 0 is 1, as required. Now, let's apply the successor function to this set,

s({∅}) = s(s(∅)) = {∅,{∅}}

Note that #{∅,{∅}} = 2. Let's do a couple more,

s({∅,{∅}}) = s(s(s(∅))) = {∅,{∅},{∅,{∅}}} with #{∅,{∅},{∅,{∅}}} = 3

and

s({∅,{∅},{∅,{∅}}}) = s(s(s(s(∅)))) = {∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}} with #{∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}} = 4

and so on...

We now have a nice set theoretical definition of the meaning of digits for the natural numbers:

0 → ∅
1 → {∅}
2 → {∅,{∅}}
3 → {∅,{∅},{∅,{∅}}}
4 → {∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}}
...

Furthermore, we have that

∅ ⊂ {∅} ⊂ {∅,{∅}} ⊂ {∅,{∅},{∅,{∅}}} ⊂ {∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}} ⊂ ...

as required! That means that our notion of natural numbers is independent of the digits that we use to write them.

Now back to the powersets. It turns out that,

P(∅) = {∅} = s(∅)
P(P(∅)) = P({∅}) = {∅,{∅}} = s(s(∅))
P(P(P(∅))) = P({∅,{∅}}) = {∅,{∅},{∅,{∅}}} = s(s(s(∅)))

However,

P(P(P(P(∅)))) ≠ s(s(s(s(∅))))

From above,

P(P(P(P(∅)))) = P({∅,{∅},{∅,{∅}}}) = {∅,{∅},{∅,{∅}},{{∅},{∅,{∅}},{∅,{∅,{∅}}},{∅,{∅},{∅,{∅}}}} ≠ s(s(s(s(∅))))

That means repeatedly applying the powerset constructor P to the empty set does not create the natural numbers the way the successor function does. It only is true for the first 3 applications where P and s coincide.

[9/6/16] NOTE: New room: Centr for Biotec & Life Sci 152
[9/3/16] Welcome!

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.

Documents of Interest:

Literature Pointers


NOTE: email submissions are not acceptable for assignments.

Assignments: