I. Introduction to Operational Semantics
 A. definition
------------------------------------------
    OPERATIONAL SEMANTICS

def: an operational semantics of
 a language L is:


------------------------------------------
	Have we made any progress in defining L?
	what's an example?
 B. advantages
  1. applications to compilation
  2. easiest kind of semantics to write down
  3. best for semantics of concurrency (it seems)
 C. problems
  1. well-definedness
  2. using the semantics to reason about a program in the original language
 D. remarks
 E. Things to think about specifying
II. Structural operational semantics
 A. two styles
------------------------------------------
STYLES OF STRUCTURAL OPERATIONAL SEMANTICS

   names              better for




------------------------------------------
 B. evaluation, big step, or natural semantics
  1. idea
------------------------------------------
   EVALUATION (BIG STEP) SEMANTICS

evaluation relation:
    evalsto is a


idea: 
------------------------------------------
  2. example
------------------------------------------
        EXAMPLE: ARITHMETIC EXPRESSIONS

Concrete Syntax:

   <exp> ::= <int> | <exp> <op> <exp>
   <op> ::= + | - | *

Abstract Syntax:






------------------------------------------
        How could we code the abstract syntax for this in Haskell?
------------------------------------------
    % abstract syntax for arithmetic

% concrete syntax:
%   <exp> ::= <int> | <exp> <op> <exp>
%   <op> ::= + | - | *

module arith_abstract_syntax.

kind exp	type.
kind operator	type.

% abstract syntax
type	add	operator.
type	sub	operator.
type	mult	operator.
type	num	int -> exp.
type	op	operator -> exp -> exp
			-> exp.
------------------------------------------
------------------------------------------
% Evaluation semantics adapted from
% M. Hennessy: The Semantics of
% Programming Languages (Wiley, 1990).

module arith.

import arith_abstract_syntax.

% auxilliary semantic relations
type	ap	operator -> int -> int
			 -> int -> o.

(ap add N1 N2 Ans) :- Ans is N1 + N2.
(ap sub N1 N2 Ans) :- Ans is N1 - N2.
(ap mult N1 N2 Ans) :- Ans is N1 * N2.

% the evalsto relation
type	evalsto	exp -> int -> o.

     (evalsto (num N) N).


=> % ----------------------------------
     (evalsto (op Oper E1 E2) Ans).
------------------------------------------
   a. notational issues
	can you show the proof for:
		(op mult (num 10) (op sub (num 5) (num 3)))?
   b. side conditions and other variations
        What is the best way to show use of side-conditions in proofs?
   c. dealing with errors
	Can you add division to this?  What about division by zero?
 C. terminal transition system, little step, computation semantics
  1. idea
------------------------------------------
   COMPUTATION (LITTLE STEP) SEMANTICS

	      Meaning
    Programs <-------> Answers







def: a in Meaning[[P]] iff



------------------------------------------
  2. terminal transition systems
------------------------------------------
    TERMINAL TRANSITION SYSTEM (TTS)

(Gamma, reducesto, T)

Gamma: 

reducesto: 

T: 




reducesto*
	reflexive, transitive closure
------------------------------------------
  3. example: arithmethic expressions
------------------------------------------
      COMPUTATIONAL SEMANTICS
     OF ARITHMETIC EXPRESSIONS

Programs = <exp>
Gamma = 
T = 
Answers = int

input[[P]] = 
output[[(num N)]] =
------------------------------------------
------------------------------------------
module comput_arith.

% Computation semantics for the language
% of arithmetic expressions. Adapted
% from M. Hennessy: The Semantics of
% Programming Languages (Wiley, 1990).

import arith_abstract_syntax.

% auxilliary semantic relations
type    output  exp -> int -> o.        
(output (num N) N).

type    ap      operator -> int -> int
			 -> int -> o.
(ap add N1 N2 Ans) :- Ans is N1 + N2.
(ap sub N1 N2 Ans) :- Ans is N1 - N2.
(ap mult N1 N2 Ans) :- Ans is N1 * N2.

% the reducesto relation
type    reducesto       exp -> exp -> o.

            (ap Oper V1 V2 N)
=> % ------------------------------------
    (reducesto (op Oper (num V1) (num V2))
               (num N)).

          (reducesto E1 V1)
=> % ----------------------------
      (reducesto (op Oper E1 E2)
                 (op Oper V1 E2)).

          (reducesto E2 V2)
=> % --------------------------
     (reducesto (op Oper E1 E2)
                (op Oper E1 V2)).
------------------------------------------
	how would you describe the order of evaluation?
	what has to be done?
  4. Example: the lambda calculus
------------------------------------------
            SYNTAX OF
   THE UNTYPED LAMBDA CALCULUS

  M ::=			     term
       I		       identifier
     | (\I . M)                abstraction
     | (M1 M2)                 application
------------------------------------------
        Is this an abstract or concrete syntax?
------------------------------------------
      COMPUTATIONAL SEMANTICS
      OF LAMBDA CALCULUS TERMS

Programs = LambdaTerm
Gamma = 
T = 
Answers = 

input[[M]] = 
output[[M]] = 

------------------------------------------
   a. axioms for transitions and inference rules
------------------------------------------
    TRANSITION AXIOMS AND RULES

[beta] ((\I.M) N) --> 


[eta]  (\I.(M I)) -->



[reduce-body] ------------------
              (\I.M) --> (\I.M')


[app-operator] ----------------
               (M N) --> (M' N)


[app-operand]  ----------------
               (M N) --> (M N')
------------------------------------------
        Is this little step or big step?
	Can you trace the execution of (((\x.(\y. (y x))) i) z)?
        What is the meaning of ((\x. (x x)) (\x.x))?
        What is the meaning of ((\x.(x f)) (\x.(z x))?
	What is the meaning of ((\x.(x x)) (\x.(x x)))?
   b. remarks
   c. variations
 D. Nondeterminism
	how would you specify angelic, demonic nondeterminism?
 E. process calculi
III. operational semantics of recursion
 A. adding recursion to the lambda calculus
------------------------------------------
    RECURSION IN OPERATIONAL SEMANTICS
           OF THE \-CALCULUS

Extended abstract syntax:

	M, N \in LambdaTerm
	I    \in Identifier

	M ::= I
              | (\ I . M) | (M N)
	      | (rec I = M)

Additional Transition Axioms:

[unroll] (rec I = M) --> 

Example:
   (rec fact =
      (\n . (((IF (eq n 0)) 1)
               ((mult n)
                 (fact ((sub n) 1))))))
 -->
   (\n . (((IF (eq n 0)) 1)
      ((mult n)
        ((rec fact =
         (\n . (((IF (eq n 0)) 1)
               ((mult n)
                 (fact ((sub n) 1))))))
                   ((sub n) 1)))))
------------------------------------------
	can you "simplify"
		((rec ohno = (\n. (ohno n))) 3)
	   for a few transitions?
 B. while loops in an imperative language
------------------------------------------
  WHILE LOOPS IN AN IMPERATIVE LANGUAGE

Abstract Syntax:

	   L \in Location
	B, E \in Expression
	   C \in Command

	C ::= E | skip | L := E | C1 ; C2
	    | if E then C1 else C2
	    | while B do C

Computation Semantics:

	Programs = Command
	Gamma = 
	T = 
	Answers = 

	input[[C]] = 
	output(g) =
------------------------------------------
------------------------------------------
	   STORES

Domains:

       V \in Value
             Storable = Value
   Sigma \in Store = Location -> Storable

Auxiliary functions:

   empty_store: Store
   empty_store = \L.unbound

   update: Store -> Location -> Storable
                 -> Store
   update Sigma L V =
		 \L'. if L = L'
		 then V else Sigma(L')

   access: Store -> Location -> Storable
   access Sigma L = Sigma(L)
------------------------------------------
------------------------------------------
        TRANSITION AXIOMS AND RULES

Auxiliary semantic relation:

	==>e : Expression * Store
		-> Value * Store -> o

------------------------------------------
	Can you define a suitable grammar for E and a big step semantics
		for ==>e  (this should allow side effects in expressions)?
------------------------------------------
     IMPERATIVE COMMANDS PART 1

	--> : Command * Store
		-> Command * Store -> o

	    E, Sigma ==>e V, Sigma'
[exp-cmd]  -------------------------
	   E, Sigma --> skip, Sigma'


[assign]  -------------------------------
	   L := E, Sigma --> skip, Sigma''







------------------------------------------
        What rule(s) would you have for C1 ; C2 ?
	What is the semantics of L1 := 1; L2 := 2 ?
	Can you give a 2 rules for if-commands?
------------------------------------------
      IMPERATIVE COMMANDS PART 2









	    B, Sigma ==>e false, Sigma'
[whileF]  ------------------------------
      while B do C, Sigma --> skip, Sigma'


	    B, Sigma ==>e true, Sigma'
[whileT]  ------------------------------
          while B do C, Sigma
                --> C;while B do C, Sigma'
------------------------------------------
	What is the meaning of the program
		L1 := 1; while L1 < 3 do L1 := L1 + 1
	   ?
	Can you give a big step semantics for commands?
	Can you give a little step semantics for expressions and
		modify the above rules to use that?
 C. summary
IV. Structural operational semantics of BeCecil
 A. overview
  1. what has to be done
------------------------------------------
     WHAT HAS TO BE DONE TO WRITE
       A SEMANTICS FOR BECECIL?

Tasks:
   (informal understanding)
   concrete syntax
   (examples, informal explanations)
   abstract syntax
   big step or little step?
   data structures (domains)
   rules for each piece of syntax

------------------------------------------
  2. abstract syntax
        Do we want recursive declaration sequences as a type?
        What about class names?
  3. semantic domains
   a. objects
------------------------------------------
            OBJECTS

module object.

import inherits set.

% kind objectId = int.
kind object type.


------------------------------------------
        How do we make objects?  How to program oid?
   b. inheritance relationships
        Why are inheritance relationships represented as things in BeCecil?
------------------------------------------
        INHERITANCE RELATIONSHIPS

module inherits.

import finite_rel.

type leq_inh finite_rel int int
             -> int -> int -> o.

leq_inh I ID1 ID2 :- related I ID1 ID2.
leq_inh I ID ID.

((leq_inh I ID1 ID2), (leq_inh I ID2 ID3))
=> %-------------------------------------
         (leq_inh I ID1 ID3).
------------------------------------------
        Will this cause computational problems for us?
        Can you write a \Prolog rule for ancestors membership (figure A-4)?
   c. generic functions
   d. contexts, environments, elaborateds
   e. stores
  4. rules
        How would you write a little step semantics for BeCecil?
V. Operational semantics summary
 A. good points of operational semantics
	what are some of the good points of operational semantics?
 B. problems with operational semantics
	what are some of the bad points of operational semantics?