types 

Addr = token;
Data = token;

Memory :: addrs: set of Addr
          mapx: map Addr to Data;

MainMemory = Memory;

Cache :: addrs: set of Addr
         mapx: map Addr to Data
         dirty: set of Addr;

System :: cache: Cache
          main: MainMemory
inv system == system.cache.addrs subset system.main.addrs



functions

badAddrs : System -> set of Addr
badAddrs (s) == { x | x in set s.cache.addrs &
                      s.cache.mapx(x) <> s.main.mapx(x) };

load : System * Addr -> System
load (s, a) == mk_System(
                        mk_Cache(s.cache.addrs union {a},
                                 s.cache.mapx munion { a |-> s.main.mapx(a) },
                                 s.cache.dirty),
                        s.main)
pre a not in set s.cache.addrs;

systemWrite : System * Data * Addr -> System
systemWrite (s, d, a) == 
        mk_System (
                mk_Cache(s.cache.addrs,
                         s.cache.mapx ++ { a |-> d },
                         s.cache.dirty union {a} ),
                s.main);

flush : System -> System
flush (s) == let x in set s.cache.addrs
             in mk_System(
                        mk_Cache(s.cache.addrs \ {x},
                                 {x} <-: s.cache.mapx,
                                 s.cache.dirty \ {x}),
                        mk_Memory(s.main.addrs,
                                  s.main.mapx ++ { x |-> s.cache.mapx(x)}))