CleanWhile

Clean While tools

This module provides types and tools to work with While in Clean. Features include:

Types for While statements, arithmetic and boolean expressions, states, derivation trees and derivation sequences
semi-prettyprint toString for those types
Evaluating statements in states
Constructing derivation trees and sequences according to the rules of Natural and Structural Operational Semantics as defined by Nielson & Nielson

Example: square root

For example, the following program is a rounded down square root function (if x=n at the start and n is a natural number, then z is the square root of n, rounded down, after execution):

import While
from WhileVars import o, s, x, z // o :== Var 'o'; etc.

sqrt :: Stm
sqrt = z := 0 :.
       o := 1 :.
       s := 1 :.
       While (s <= x)
         ( z := z + 1 :.
           o := o + 2 :.
           s := s + o )

Evaluation

We can now execute this code on a State, which maps Var to Int:

Start :: Int
Start = eval NS sqrt st z
where
    st :: Char -> Int  // Or: st :: Var -> Int  // st :: CharState
    st 'x' = 9         //     st (Var 'x') = 9  // st = \'x' -> 9

eval NS sqrt st is a State itself (the state that results from execution of sqrt in st), so we apply that to z to get the result. Other than the documentation of While suggests, a State can be a partial function here. There is no efficient way of enforcing total functions in Clean.

The NS argument tells the module to use Natural Semantics (as opposed to SOS, Structural Operational Semantics). The result should be the same (though this has not been heavily tested, it has been proven for the derivation rules that define NS and SOS, and the functions in this module are directly derived from those rules). These two semantics are defined for While by Nielson and Nielson in Semantics with Applications: A Formal Introduction.

Constructing derivation trees and sequences

Besides evaluating statements, we can also construct derivation trees and sequences. The following two Start rules generate a derivation tree for Natural Semantics and a derivation sequence for Structural Operational Semantics. Both types can be toStringed:

Start = tree sqrt st
Start = seq sqrt st

For example, the tree for sqrt in st with st x = 9 (when passed to toString):

(z:=0; o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
  z:=0
  (o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
    o:=1
    (s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
      s:=1
      (while s<=x do (z:=z+1; o:=o+2; s:=s+o)
        (z:=z+1; o:=o+2; s:=s+o
          z:=z+1
          (o:=o+2; s:=s+o
            o:=o+2
            s:=s+o
          )
        )
        (while s<=x do (z:=z+1; o:=o+2; s:=s+o)
          (z:=z+1; o:=o+2; s:=s+o
            z:=z+1
            (o:=o+2; s:=s+o
              o:=o+2
              s:=s+o
            )
          )
          (while s<=x do (z:=z+1; o:=o+2; s:=s+o)
            (z:=z+1; o:=o+2; s:=s+o
              z:=z+1
              (o:=o+2; s:=s+o
                o:=o+2
                s:=s+o
              )
            )
            while s<=x do (z:=z+1; o:=o+2; s:=s+o)
          )
        )
      )
    )
  )
)

And the sequence:

z:=0; o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
skip

As you can see, neither method outputs the states. Since a State is actually a function (and not a [(Var, Int)], for example), it is impossible to toString a State an sich. It may be possible to toString states in the context of a derivation tree or sequence, by looking for the variables present or modified. This is something for a next version.

Warning

This breaks StdEnv completely. Only import what you need, as always, and use qualified imports where needed.

Todo

Gast testing
Prettyprint for DerivTree
Parser
Add the state to the toString of DerivTree and DerivSeq
Easy interface for While language extensions