*** ___________________________________________________________________________
***
***  file: ~/Teaching/COMP317/Maude/simpleSemantics.maude
***
*** ___________________________________________________________________________
***
***  Author: Grant Malcolm
***
***   This code may be freely used, distributed or modified,
***   provided due credit be given.
***
*** ___________________________________________________________________________
***
***
***  The semantics of SIMPLE.
***
***
*** ___________________________________________________________________________
***



*** *************************************************************************
***  Theory of storage.
***
***  This theory specifies the "state" of an abstract machine that can
***  execute SIMPLE programs.
***  The state consists of the values stored in variables,
***  and can be thought of as a table.
***  There is an operation to get the value of a variable,
***  which can be thought of as table look-up;
***  and an operation to update the value in the table
***  - this is the assignment operation.
***
th  STORE  is

    *** Using SIMPLE's basic programs.
    ***
  protecting  BASIC_PROGRAMS .

    *** Using Maude's built-in integers.
    ***
  protecting  INT .


    *** States of abstract machines that run SIMPLE programs.
    ***
  sort  Store .


    *** Initial state of an abstract machine.
    ***
  op  initial  : -> Store .


    *** "Look up" the value of a variable.
    ***  In fact, rather than declaring this as an operation
    ***  of type  Store Variable -> Int ,
    ***  we generalise this by saying we can evaluate any Expression,
    ***  not just a variable.
    ***
  op  _[[_]]  : Store Expression -> Int
              [ prec 75 ] .


    *** "Update" a state (by assigning to a variable).
    ***
  op  _;_ : Store BasicProgram -> Store
          [  prec 70 ] .



  var  S : Store .
  vars V V' : Variable .
  vars E E' : Expression .

    *** Initially, all variables store 0:
    ***
  eq  initial [[ V ]]  =  0 .


    *** evaluate binary operations, by evaluating their operands
    *** and combining the results (by addition, multiplication, etc.)
    ***
  eq  S [[ E + E' ]]  =  (S [[ E ]]) + (S [[ E' ]]) . 
  eq  S [[ E * E' ]]  =  (S [[ E ]]) * (S [[ E' ]]) . 
  eq  S [[ E - E' ]]  =  (S [[ E ]]) - (S [[ E' ]]) .


    *** evaluate unary minus by evaluating the operand,
    *** then taking the minus
    ***
  eq  S [[ (- E) ]]  =  - (S [[ E ]]) .


    ***  evaluate digits in the obvious way...
    ***
  eq  S [[ 0 ]]  =  0 .
  eq  S [[ 1 ]]  =  1 .
  eq  S [[ 2 ]]  =  2 .
  eq  S [[ 3 ]]  =  3 .
  eq  S [[ 4 ]]  =  4 .
  eq  S [[ 5 ]]  =  5 .
  eq  S [[ 6 ]]  =  6 .
  eq  S [[ 7 ]]  =  7 .
  eq  S [[ 8 ]]  =  8 .
  eq  S [[ 9 ]]  =  9 .


  var  N : Numeral .
  var  D : Digit .


    ***  ...and use the place system to evaluate numerals
    ***  
  eq  S [[ N D ]]  =  10 * (S[[ N ]]) + (S[[ D ]]) .


    *** an assignment updates the value associated with the variable ...
    ***
  eq  S ; V := E [[ V ]]  =  S [[ E ]] .


    *** ... and only that variable
    ***
  cq S ; V := E [[ V' ]]  =  S [[ V' ]]   if V =/= V' .

endth



*** *************************************************************************
***  Some useful properties of arithmetic operations.
***  These are used in proof scripts for program verification.
***
fmod  ZZ  is

  protecting  INT .  *** using Maude's built-in integers

    *** equality test for integers
    ***
  op  _is_ : Int Int -> Bool .


  vars  I J K L : Int .

    *** properties of arithmetic operations

  eq   0 + I  =  I .
  eq   I + - I  =  0 .
  eq   -(I + J)  =  - I + - J .
  eq   I - J  =  I + (- J) .
  eq   0 * I  =  0 .
  eq   - I * J  =  -(I * J) .
  eq   I * (J + K)  =  I * J + I * K .
  eq   (I + J) * K  =  I * K + J * K .
  cq   I * J  =  (I - 1)* J + J   if  I > 0 .

    *** properties of arithmetic relations
  eq   I is I  =  true .
  cq   I is J  =  false   if  I < J  or  J < I .
  eq   (I + J) is (K + J)  =  I is K .
  eq   (I * J) is (K * J)  =  I is K .
  eq   (I - J) is (K - J)  =  I is K .

  eq  not(I <= J)  =  J < I .
  eq  not(I < J)  =  J <= I .

  eq   I + 1 <= J  =  I < J .
  eq   I < J + 1  =  I <= J .
  eq   I <= J + -1  =  I < J .
  eq   I <= J + - K  =  I + K <= J .
  eq   I < J + - K  =  I + K < J .
  eq   I + -1 < J  =  I <= J .
  eq   I <= I  =  true .
  eq   I < I  =  false .
  cq   I < I + J  =  true   if  0 < J .
  eq   I + -1 < I  =  true .
  cq   I + J < I  =  true   if  J < 0 .
  cq   I <= J  =  true   if  I < J .
  cq   I <= J + 1  =  true  if  I <= J .
  cq   I <= J + K  =  true  if  I <= J  and  I <= K .
  cq   I + J <= K + L  =  true  if  I <= K  and  J <= L .

endfm



*** *************************************************************************
***  Semantics of SIMPLE.
***
***  The semantics of SIMPLE programs is described by saying
***  how programs update Stores.
***

th SEMANTICS is

  protecting  PROGRAMS .
  protecting  ZZ .
  including   STORE .


    ***  An error supersort to contain "undefined" stores
    ***  such as:  initial ; while true do skip od
    ***
  sort  ErrorStore .

    ***  ErrorStore contains all the well-defined stores,
    ***  such as those produced by programs that terminate,
    ***  as well as all the "undefined" stores that "result"
    ***  from programs that don't terminate.
    ***
  subsort  Store < ErrorStore .


    ***  To evaluate boolean expressions
    ***  Results are of Maude's built-in sort Bool,
    ***  from the built-in module BOOL
    ***
  op  _[[_]] : Store BooleanExpression -> Bool
             [ prec 75 ] .


  var  S : Store .
  vars E1 E2 : Expression .
  vars T1 T2 : BooleanExpression .

    *** evaluation of boolean expressions
    ***
  eq  S [[ E1 < E2 ]]  =  (S [[ E1 ]]) < (S [[ E2 ]]) .
  eq  S [[ E1 <= E2 ]]  =  (S [[ E1 ]]) <= (S [[ E2 ]]) .
  eq  S [[ E1 == E2 ]]  =  (S [[ E1 ]]) is (S [[ E2 ]]) .
  eq  S [[ T1 or T2 ]]  =  (S [[ T1 ]]) or (S [[ T2 ]]) .
  eq  S [[ T1 and T2 ]]  =  (S [[ T1 ]]) and (S [[ T2 ]]) . 
  eq  S [[ not T1 ]]  =  not (S [[ T1 ]]) .
  eq  S [[ true ]]  =  true .
  eq  S [[ false ]]  =  false .


    ***  Run program P in a store S to obtain new store S ; P .
    ***  ErrorStore is used to allow for non-terminating programs.
    ***
  op  _;_ : ErrorStore Program -> ErrorStore [prec 70] .


  var T : BooleanExpression . 
  var P1 P2 : Program . 

    *** execution of programs

    ***  skip has no effect on Stores
    ***
  eq  S ; skip  =  S .

    ***  Sequential composition:
    ***  do first program, then do the next
    ***
  eq  S ; (P1 ; P2)  =  (S ; P1) ; P2 .

    ***  Conditionals:
    ***  if test is true, execute the then-clause...
    ***
  cq   S ; if T then P1 else P2 endif  =  S ; P1
    if  S[[T]] .

    ***  ... otherwise, execute the else-clause
    ***
  cq   S ; if T then P1 else P2 endif  =  S ; P2
    if  not(S[[T]]) .

    ***  While-loops:
    ***  if guard is true, execute the body, and repeat ...
    ***
  cq   S ; while T do P1 od  =  S ; P1 ; while T do P1 od 
    if  S[[T]] .

    ***  ... otherwise, exit the loop (do nothing)
    ***
  cq   S ; while T do P1 od  =  S
    if  not(S[[T]]) .

endth