Imperative Action Notation

Actions

store Y | unstore Y | reserve Y | unreserve Y

• All primitive imperative actions:
  
  
  • Give no transients.
    
    
  • Produce no bindings.
    
    
  • Do not communicate.
    
    
  • Redirect no bindings.
    
    
• There are no special imperative action combinators.
  
  
• storeY₁ in Y₂: a primitive imperative action, where Y₁ is a yielder of storable data and Y₂ is a yielder of cells. Represents changing an atomic piece of stable information.
  
  
  • Indivisible. Commits and completes when Y₂ yields a reserved cell and Y₁ yields storable data. Fails otherwise.
    
    
  • Stores the storable yielded by Y₁ in the cell yielded by Y₂.
    
    
• unstoreY: a primitive imperative action, where Y is a yielder of cells. Represents destroying a piece of stable information.
  
  
  • Indivisible. Commits and completes when Y yields a reserved cell. Fails otherwise.
  • Stores the datum uninitialized in the cell yielded by Y.
    
    
• reserve Y: a primitive imperative action, where Y is a yielder of cells. Represents extending stable information with an extra, uninitialized piece.
  
  
  • Indivisible. Commits and completes when Y yields an unreserved cell. Fails otherwise.
    
    
  • Reserves the cell yielded by Y and stores the datum uninitialized in it.
    
    

• unreserve Y: a primitive imperative action, where Y is a cell yielder. Represents destroying stable information.
  
  
  • Indivisible. Commits and completes when Y yields a reserved cell. Fails otherwise.
    
    
  • Unreserves the cell yielded by Y.
    
    

  Actions| Yielders| Data

Yielders

current storage | the d stored in Y

• current storage:current storagecurrent storage a yielder of storage maps. Yields the state of storage.
  
  
• the d stored in Y: a yielder of storable data, where d is a sort of data and Y is a yielder of cells. Yields the data of sort d stored in the cell yielded by Y according to the current storage, provided that the cell is currently reserved.
  

  Actions| Yielders| Data

  
  

storage | cell | storable | uninitialized | initialized S

• storage: a subsort of map. Its individuals represents states of stable information, associating cells with storable (or uninitialized) individuals.
  
  
• cell: a subsort of distinct-datum. Its individuals represent the locations of pieces of stable information. Left loosely-specified, as the details are implementation-dependent.
  
  
• storable: a subsort of data. Left unspecified, as it depends on the variety of stable information processed by the programs of a programming language.
  
  
• uninitialized: an individual datum. Represents the absence of a stored datum in a reserved cell.
  
  
• initialized S: the restriction of the storage S obtained by omitting uninitialized cells.
  

  Actions| Yielders| Data