Tyler Hall Rm 251

Office hours: Monday 11-noon Tyler 251, Wednesday 1-2pm Tyler 251, or by appointment

email: hamel@cs.uri.edu

[12/15/16] posted all solutions for csc501 including solutions to the EC midterm and assignment #6.

[12/12/16]

[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]

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]

[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 ⇔ BSo, 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!

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

- We can formally establish that a programming language implementation is correct.
- We obtain a mathematically precise description of the behavior of every feature in the programming language under consideration.

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.

- Wikipedia's take on the topic
- Rewriting Tutorial by N. Dershowitz
- Natural Semantics by Gilles Kahn
- Structured Operational Semantics by Gordon Plotkin
- Denotational Semantics by David Schmidt (the figures for chapter 1 can be found here)
- Benjamin Pierce's Great Works in Programming Languages
- Book: Semantics with Applications (a primer)
- Book: The Formal Semantics of Programming Languages (a classic, mathematically demanding)

NOTE: email submissions are not acceptable for assignments.

- Assignment #1 - due on Wednesday 9/28 in Sakai.
- Assignment #2 - due on Thursday 10/13 in Sakai.
- Assignment #3 - due on Friday 10/21 in Sakai.
- Assignment #4 - due on Monday 10/31 in Sakai. Read and do all exercises in the tutorial up to and including section 3.1 except exercise 9. For exercise 1 you can assume these Prolog facts. Please upload a copy of your programs together with a log that shows that the programs execute.
- Assignment #5 - due on Thursday 11/10 in Sakai.
- Assignment #6 - due on Monday 12/12 in Sakai.