Storing

Funcons-beta : Storing.cbs | PRETTY | PDF

Outline

Storing

Storing

[
  Datatype locations                     Alias locs
  Type     stores
  Entity   store
  Funcon   initialise-storing
  Funcon   store-clear
  Datatype variables                     Alias vars
  Funcon   variable                      Alias var
  Funcon   allocate-variable             Alias alloc
  Funcon   recycle-variables             Alias recycle
  Funcon   initialise-variable           Alias init
  Funcon   allocate-initialised-variable Alias alloc-init
  Funcon   assign
  Funcon   assigned
  Funcon   current-value
  Funcon   un-assign
  Funcon   structural-assign
  Funcon   structural-assigned
]

Meta-variables
  T, T′ <: values

Stores

Type
  locations ~> atoms
Alias
  locs = locations

A storage location is represented by an atom.

Type
  stores ~> maps(locations, values^?)

The domain of a store is the set of currently allocated locations. Mapping a location to ( ) models the absence of its stored value; removing it from the store allows it to be re-allocated.

Entity
  < _ , store(_:stores) > ---> < _ , store(_:stores) >

The current store is a mutable entity. A transition < X , store(Sigma) > ---> < X′ , store(Sigma′) > models a step from X to X′ where the difference between Sigma and Sigma′ (if any) corresponds to storage effects.

Funcon
  store-clear : =>null-type
Rule
  < store-clear , store(_) > ---> < null-value , store(map( )) >

store-clear ensures the store is empty.

Funcon 
  initialise-storing(X:=>T) : =>T
   ~> sequential(store-clear, 
        initialise-giving(initialise-generating(X)))
Alias
  init-storing = initialise-storing

initialise-storing(X) ensures that the entities used by the funcons for storing are properly initialised.

Simple variables

Simple variables may store primitive or structured values. The type of values stored by a variable is fixed when it is allocated. For instance, allocate-variable(integers) allocates a simple integer variable, and allocate-variable(vectors(integers)) allocates a structured variable for storing vectors of integers, which can be updated only monolithically.

Datatype
  variables ::= variable(_:locations, _:value-types)
Alias
  vars = variables

Alias
  var = variable

variables is the type of simple variables that can store values of a particular type.

variable(L, T) constructs a simple variable for storing values of type T at location L. Variables at different locations are independent.

Note that variables is a subtype of datatype-values.

Funcon
  allocate-variable(T:types) : =>variables
Alias
  alloc = allocate-variable

allocate-variable(T) gives a simple variable whose location is not in the current store. Subsequent uses of allocate-variable(T′) give independent variables, except after recycle-variables(V,...) or store-clear.

Rule
  < use-atom-not-in(dom(Sigma)) , store(Sigma) > ---> < L , store(Sigma′) >
  map-override({L |-> ( )}, Sigma′) ~> Sigma′′
  -------------------------------------------------------------------------
  < allocate-variable(T:types) , store(Sigma) >
    ---> < variable(L, T) , store(Sigma′′) >

Funcon
  recycle-variables(_:variables⁺) : =>null-type
Alias
  recycle = recycle-variables

recycle-variables(Var,...) removes the locations of Var, …, from the current store, so that they may subsequently be re-allocated.

Rule
  is-in-set(L, dom(Sigma)) == true
  ---------------------------------------------------------------------
  < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
    ---> < null-value , store(map-delete(Sigma, {L})) >
Rule
  is-in-set(L, dom(Sigma)) == false
  ---------------------------------------------------------------------
  < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >
Rule
  recycle-variables(Var:variables, Var⁺:variables⁺)
    ~> sequential(recycle-variables(Var), recycle-variables(Var⁺))

Funcon
  initialise-variable(_:variables, _:values) : =>null-type
Alias
  init = initialise-variable

initialise-variable(Var, Val) assigns Val as the initial value of Var, and gives null-value. If Var already has an assigned value, it fails.

Rule
  and(is-in-set(L, dom(Sigma)),
      not is-value(map-lookup(Sigma, L)),
      is-in-type(Val, T)) 
    == true
  ----------------------------------------------------------------------------
  < initialise-variable(variable(L:locations, T:types), Val:values) , 
    store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
Rule
  and(is-in-set(L, dom(Sigma)),
      not is-value(map-lookup(Sigma, L)),
      is-in-type(Val, T)) 
    == false
  ----------------------------------------------------------------------------
  < initialise-variable(variable(L:locations, T:types), Val:values) , 
    store(Sigma) > ---> < fail , store(Sigma) >

Funcon
  allocate-initialised-variable(T, Val:T) : =>variables
    ~> give(allocate-variable(T),
         sequential(initialise-variable(given, Val), given))
Alias
  alloc-init = allocate-initialised-variable

allocate-initialised-variable(T, Val) allocates a simple variable for storing values of type T, initialises its value to Val, and returns the variable.

Funcon
  assign(_:variables, _:values) : =>null-type

assign(Var, Val) assigns the value Val to the variable Var, provided that Var was allocated with a type that contains Val.

Rule
  and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == true
  -----------------------------------------------------------------------
  < assign(variable(L:locations, T:types), Val:values) ,
    store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
Rule
   and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == false
  --------------------------------------------------------------------------
  < assign(variable(L:locations,T:types), Val:values) ,
    store(Sigma) > ---> < fail , store(Sigma) >

Funcon
  assigned(_:variables) : =>values

assigned(Var) gives the value assigned to the variable Var, failing if no value is currently assigned.

Rule
  map-lookup(Sigma, L) ~> (Val:values)
  ------------------------------------------------------------------
  < assigned(variable(L:locations, T:types)) , store(Sigma) >
    ---> < Val , store(Sigma) >
Rule
  map-lookup(Sigma, L) == ( )
  ------------------------------------------------------------------
  < assigned(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >

Funcon
  current-value(_:values) : =>values

current-value(V) gives the same result as assigned(V) when V is a simple variable, and otherwise gives V.

It represents implicit dereferencing of a value that might be a variable.

Rule
  current-value(Var:variables) ~> assigned(Var)
Rule
  current-value(U:~variables) ~> U

Funcon
  un-assign(_:variables) : =>null-type

un-assign(Var) remove the value assigned to the variable Var.

Rule
  is-in-set(L, dom(Sigma)) == true
  --------------------------------------------------------------------------
  < un-assign(variable(L:locations, T:types)) , store(Sigma) >
    ---> < null-value , store(map-override({L |-> ( )}, Sigma)) >
Rule
   is-in-set(L, dom(Sigma)) == false
  --------------------------------------------------------------------------
  < un-assign(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >

Structured variables

Structured variables are structured values where some components are simple variables. Such component variables can be selected using the same funcons as for selecting components of structured values.

Structured variables containing both simple variables and values correspond to hybrid structures where particular components are mutable.

All datatypes (except for abstractions) can be used to form structured variables. So can maps, but not sets or multisets.

Structural generalisations of assign(Var, Val) and assigned(Var) access all the simple variables contained in a structured variable. Assignment requires each component value of a hybrid structured variable to be equal to the corresponding component of the structured value.

Funcon
  structural-assign(_:values, _:values) : =>null-type

structural-assign(V₁, V₂) takes a (potentially) structured variable V₁and a (potentially) structured value V₂. Provided that the structure and all non-variable values in V₁ match the structure and corresponding values of V₂, all the simple variables in V₁ are assigned the corresponding values of V₂; otherwise the assignment fails.

Rule
  structural-assign(V₁:variables, V₂:values)
    ~> assign(V₁, V₂)
Rule
  V₁ : ~(variables)
  V₁ ~> datatype-value(I₁:identifiers, V₁^*:values^*)
  V₂ ~> datatype-value(I₂:identifiers, V₂^*:values^*)
  -----------------------------------------------------------------------
  structural-assign(V₁:datatype-values, V₂:datatype-values)
    ~> sequential(
         check-true(is-equal(I₁, I₂)),
         effect(tuple(interleave-map(
           structural-assign(tuple-elements(given)),
           tuple-zip(tuple(V₁^*), tuple(V₂^*))))),
         null-value)

Note that simple variables are datatype values.

Rule
  dom(M₁) == {}
  ------------------------------------------------------
  structural-assign(M₁:maps(_,_), M₂:maps(_,_))
    ~> check-true(is-equal(dom(M₂), { }))
Rule
  some-element(dom(M₁)) ~> K
  ----------------------------------------------------------------------------
  structural-assign(M₁:maps(_, _), M₂:maps(_, _))
    ~> sequential(check-true(is-in-set(K, dom(M₂))),
         structural-assign(map-lookup(M₁, K), map-lookup(M₂, K)),
         structural-assign(map-delete(M₁, {K}), map-delete(M₂, {K})))
Rule
  V₁ : ~(datatype-values|maps(_, _))
  ---------------------------------------------------------------
  structural-assign(V₁:values,V₂:values)
    ~> check-true(is-equal(V₁, V₂))

Funcon
  structural-assigned(_:values) : =>values

structural-assigned(V) takes a (potentially) structured variable V, and computes the value of V with all simple variables in V replaced by their assigned values, failing if any of them do not have assigned values.

When V is just a simple variable or a (possibly structured) value with no component variables, structural-assigned(V) gives the same result as current-value(V).

Rule
  structural-assigned(Var:variables) ~> assigned(Var)
Rule
  V : ~(variables)
  V ~> datatype-value(I:identifiers, V^*:values^*)
  ----------------------------------------------------------------------------
  structural-assigned(V:datatype-values)
    ~> datatype-value(I, interleave-map(structural-assigned(given), V^*))

Note that simple variables are datatype values.

Rule
  structural-assigned(M:maps(_, _))
    ~> map(interleave-map(structural-assigned(given), map-elements(M)))
Rule
  U : ~(datatype-values|maps(_, _))
  ------------------------------------------
  structural-assigned(U:values) ~> U

From the PLanCompS Project

CBS-beta issues…

Suggest an improvement…

← ↑ →