# POCS.Lab1.VariablesAPI

# Specification of Variables.

The values of these variables are the spec state:

The precondition for read is a function that takes two arguments: a pair
(count,sum) and a spec state state and asserts a proposition about them. The
way to read this is that the precondition states that there exists a pair
(count,sum) and a state such that the value of StateCount state is count and
StateSum state is sum.
The postcondition states the value returned by read is either count or
sum, depending on which variable is read.

Definition read_spec v : Specification _ _ unit _ :=

fun (_ : unit) state => {|

pre := True;

post := fun r state' =>

state' = state /\

match v with

| VarCount => r = StateCount state

| VarSum => r = StateSum state

end;

recovered := fun _ _ => False

|}.

An implementation of write has the same precondition as read. The
postcondition states that the new spec state has either StateCount
or StateSum is updated, depending on which variable write writes. The
return value is tt.

Definition write_spec v val : Specification _ _ unit _ :=

fun (_ : unit) state => {|

pre := True;

post := fun r state' =>

r = tt /\

match v with

| VarCount => state' = mkState val (StateSum state)

| VarSum => state' = mkState (StateCount state) val

end;

recovered := fun _ _ => False

|}.

# Variables module

Module Type VarsAPI.

Axiom init : proc InitResult.

Axiom read : var -> proc nat.

Axiom write : var -> nat -> proc unit.

Axiom recover : proc unit.

Axiom abstr : Abstraction State.

(* Note that inited_any allows any initial state, meaning StatDB is required

to initialize its variables appropriately. *)

Axiom init_ok : init_abstraction init recover abstr inited_any.

Axiom read_ok : forall v, proc_spec (read_spec v) (read v) recover abstr.

Axiom write_ok : forall v val, proc_spec (write_spec v val) (write v val) recover abstr.

Axiom recover_wipe : rec_wipe recover abstr no_crash.

Hint Resolve init_ok : core.

Hint Resolve read_ok : core.

Hint Resolve write_ok : core.

Hint Resolve recover_wipe : core.

End VarsAPI.