CSCI 431 Lecture Notes - Semantics

Semantics

What does

     X.pay := X.pay + 1600 ;

What does

      DO 100 I = 1, J
 100  A(I) = I

How about?

     I := 1
     J := 2 ;
     while (I < J) do
     begin
        I := I+1 ;
        J := J+1 ;
     end

In the early days

• In the early days, we were often imprecise, but with portability?
• One solution, it's however the compiler on the S/360 in Poughkeepsie does it...
• To understand PL/I, you must understand S/360 assembler language ... Not an improvement
• Also, maybe this is too precise
  • should the result be the same on 32 and 64 bit machines?
  • should people depend on weird machine dependencies
  • what if there is a bug in the compiler?

Semantic Models

• Programs are built out of commands like assignment, conditionals, etc.
• The action of a program is to map from an acceptable initial state to an acceptable final state
• A formal model can be used as the basis for rigorous discussion
  • The rules used are described and followed very precisely

VDL -- Vienna Definition Language

• An implementation of operational semantics from the 1970's
• To define PL/I, show how to translate it into VDL
• It defines how the programming language is implemented on a virtual machine
• The changes that occur in the machine's state when it executes a given statement define the meaning of that statement.
• Basically, you get a 400-page unreadable definition

Axiomatic Semantics

• Defined in conjunction with the development of a method to prove the correctness of programs
• C.A.R Hoare introduced the following notation called a partial correctness specification for specifying what a program does:

                     {P} S {Q}
                        or
    { precondition } statements { postcondition }
  

  where:
  • S is a program
  • P and Q are conditions on the program variables used in S
  • The conditions P and Q are logical expressions called assertions
• Developing the axiomatic description of a program (or proof) requires that every statement in the program have both a precondition and postcondition

Notation

• Conditions on the program variables are written using standard mathematical notations together with logical operators like:
  • ^ (and), | (or), ~ (not), => (implies)
• Hoare's original notation was P {S} Q not {P} S {Q}, but the later is more frequently used

The Basic Idea

• {P} S {Q} is true if
  • whenever S is executed in a state satisfying P
  • and if the execution of S terminates
  • then the state in which S terminates satisfies Q

Example: {X=1} X:=X+1 {X=2}

• P is the condition that the value of X is 1
• Q is the condition that the value of X is 2
• S is the assignment command X:=X+1
• {X=1} X:=X+1 {X=2} is clearly true

Formal Specification

• {X=x ^ Y=y} S {X=y ^ Y=x}

• The statement sequence: BEGIN R:=X; X:=Y; Y:=R; END would fulfill the specification
• The statement sequence: BEGIN X:=Y; Y:=X; END would not fulfill the specification

A formal Proof

• A proof consists of a sequence of lines
• Each line is an instance of an axiom, or follows from the previous lines by a rule of inference
• An example proof for the statement: (X+1)² = X² + 2 * X + 1

  1.  (X+1)2             = (X+1) * (X+1)           definition of ()2
  2.  (X + 1) * (X + 1)  = (X+1) * X + (X+1) * 1   distributive law
  3.  (X+1)2             = (X+1) * X + (X+1) * 1   substituting 2 into 1
  4.  (X+1) * 1          = (X+1)                   identity law
  5.  (X+1) * X          = X * X + 1 * X           distributive law
  6.  (X+1)2             = X * X + 1 * X + X + 1   substituting 4 and 5 into 3
  7.  1 * X              = X                       identity law
  8.  (X+1)2             = X * X + X + X + 1       substituting 7 into 6
  9.  X * X              = X2                      definition of ()2
  10. X + X              = 2 * X                   2 = 1 + 1, distributive law
  11. (X+1)2             = X2 + 2 * X + 1          substituting 9 and 10 into 8
  

Weakest preconditions

• In proving the correctness of a program, it is often easiest to work by computing preconditions from the given postconditions:

      {?} SUM := 2 * X + 1 {SUM > 1}
  

• In this way we can work from the desired postcondition at program termination back to the stated precondition to formulate a proof of program correctness
• The weakest preconditions is the least restrictive precondition that will guarantee the validity of the associated postcondition.
• For example, in the statement above, {X > 10}, {X > 50}, and {X > 100 & Y > 0}, are all valid preconditions, but the weakest of all preconditions is {X > 10}.
• Examples:

       { X = 5 } X := X+5 { X = 10 }
       { X = Z+3 } X := X+5 { X=Z+8 }
       { X = 5 & Y = 13 } X := X+5 { X=10 }
  
       { true } X := Y { X = Y }
  
       { 5 = 6 &  X = 5 } X := 6 { X = 5 }
       { false } statement { P }
            law of the excluded miracle
       if 4 = 7, then I am the pope
  
       { ? } X := Y + 3 { X = 5 }
       { ? } if X = 0 then Y := 5 { Y = 5 }  
       { ? } while X < Y do X := X + 1 { X = Y }
       { ? } X := X + X { X = 10 }
  

Assignment Statements

• To use axiomatic semantics with a given programming language either an axiom or an inference rule must be defined for each kind of statement in the language.
• Let X=E be a general assignment statement and Q be its postcondition, then P is defined by the axiom:

  
        P = QX - > E
  
  

• Example: A = B / 2 - 1 {A < 10}

  The weakest precondition is computed by substitutiong B / 2 - 1 in the assertion {A < 10} to obtain {B < 22}

Selection statements

• Selection statements must be proven for both of their cases, i.e., both the then and the else clause
• Example:

  
        if (X > 0)
           X = X - 1;
        else 
           X = X + 1;
  
  

• If the postcondition is {X > 0}, this produces the precondition {(X + 1 > 0) | (X > 1)}. Because {X > 1} = > {X > -1}, we can use {X > 1} as the precondition for the selection statement.

Loop invariants

• Computing the weakest precondition for a while loop is inherently more difficult than for a sequence of statements because the number of iterations cannot be predetermined in all cases.
• Loops are handled with inductive style proofs using loop invariants
• The loop invariant must be:
  • true at the start of the loop (it must be implied by the precondition)
  • true after each iteration of the loop
  • it must be unchanged by the loop test
  • true at loop termination
• The precondition must guarantee the loop invariant and the loop invariant must guarantee the postcondition.
• If loop termination can be shown, there is a proof for total correctness if termination is not guaranteed (but the other conditions can be met), the proof is for partial correctness
• Example:

       { ? } while X < Y do X := X + 1 { X = Y }
  

  The loop invariant is {X < = Y}