Mutable state is a change of state. This applies to non-functional languages.

Language with mutable state (imperative) must force an ordering. This is in contrast with non-mutable languages (functional) which have implicit ordering.

Functional Ordering

This forces an ordering of (f a) before (g 3)

bind x=(f a) in 
  (g 3)
== (lambda _ in (g 3)) (f a)

functional

Identifiers get their values from parameter passing
e.g. Haskell, Scheme, OCaml, ML, Common Lisp

imperative

Identifiers get their value from a shared, global state
C, C++, Java, Ada, JavaScript (basically most modern language)

The walrus operator (:=) is an assignment that updates a variable in the next state.

x := x+1 == x' = x+1

In the the x on the left of the operator is being update in the next state or second state.

Adding Mutable State to FBAE

A Seq operator
Define a store
Update eval to maintain state in addition to environment

Note

State is global. This means changes to state can affect the further running of a program.

Concrete syntax: t ; t
Abstract syntax: Seq :: FBAE -> FBAE -> FBAE

Define sequence by elaboration: Seq l r == (App (Lambda _ r) l)

eval e s (Seq l r) = do { s' <- eval e s l; eval e s' r }

State operations for FBAE

FBAE :: new FBAE | deref FBAE | set loc FBAE

loc - a new type of value for locations
new t - creates a new location, put eval t there, returns the location
deref - retrieves a values from l and returns it
set l t - store eval t in location l and returns l

Note

loc in the concrete syntax is only defined for set. There is no other real concrete syntax. The only way to produce a location is with new. This requires that all "allocated memory" have some value.

This is by design, so users don't mess with the store.

Note

PowerPC Undocumented Instructions, intel, b2 bombers

FBAE Mutable State Examples

bind m = new 5 in     [(m,->5)]
  bind n = m in       [(n,->^), (m,->5)]
    set m 6 ; deref n [(n,->^), (m,->6)]
== 6

bind m = new 5 in       [(m,->5)]
  bind n = m in         [(n,->^), (m,->5)]
    bind n = new 5 in   [(n,->5), (n,->^), (m,->5)]
      set m 6 ; deref n [(n,->5), (n,->^), (m,->5)]
== 5
The innermost bind to n shadows the outer bind to n and since the inner n points to a new location containing 5 and not the location that m points to.

bind inc = (lambda l in (set l ((deref l) +1))) in 
  bind n = new 5 in
    inc n ; deref n
== 
This inc operates on state. It takes a location and increments the value at the location by one, and returns another location not a value.

Mutable State FBAE Abstract Syntax

Info

This model for memory behaves like a linked list. This works if access time of memory is a non-factor when verifying our model. Otherwise a constant time O(1) model must be used.

type Sto = Loc -> Maybe FBAEVal

type Loc = Int

derefSto s l = (s l)

initSto :: Sto
initSto x = Nothing

setSto :: Sto -> Loc -> FBAEVal -> Sto
setSto s l v = \m -> if m==l then (Just v) else (s m)

type Store (Loc, Sto)

Loc is the last accessed memory location
Sto is our store (state)

derefStore (_, s) l = derefSto s l

initStore = (0, initSto)

initstore sets the first location to 0, which means our first useable memory location is 1.

setStore (m, s) l v = (m, setSto s l v)

newStore (l, s) = (l+1, s)

newStore creates a new value. This function manipulates the location to create a new one.

eval e s (New t) = do { (v', (l, s')) <- eval e s t;
                        return ((Loc l+1), (setStore (newStore (l,s')) s' v'))
                       }