# Library POCS.Lab1.StatDbAPI

# Specification for StatDB

- The state of the StatDB: a list of integers
- An initial state: the list of integers is nil
- Two operations: add and mean. The specification for each operation is

## The state of StatDB

## The specification of the StatDB operations

- add_spec's post condition states that add v adds v to the spec state
of StatDB and that add returns tt.
- mean_spec's post condition states that mean doesn't modify the spec state of StatDB, and that its return value is one of two values: (1) if state is nil, then the return value is None; (2) if state is not nil, then the return value is the average of the numbers in StatDB's state.

Definition add_spec v : Specification unit unit unit State :=

fun (_ : unit) state => {|

pre := True;

post := fun r state' =>

r = tt /\ state' = v :: state;

recovered := fun _ _ => False

|}.

Definition mean_spec : Specification unit (option nat) unit State :=

fun (_ : unit) state => {|

pre := True;

post := fun r state' =>

state' = state /\

(state = nil /\ r = None \/

state <> nil /\ r = Some (fold_right plus 0 state / length state));

recovered := fun _ _ => False

|}.

# StatDB module

The implementation must provide the following methods:

Axiom init : proc InitResult.

Axiom add : nat -> proc unit.

Axiom mean : proc (option nat).

Axiom recover : proc unit.

Axiom add : nat -> proc unit.

Axiom mean : proc (option nat).

Axiom recover : proc unit.

The abstraction relation between spec and code state

The proofs that the implementation methods meet their specs:

Axiom init_ok : init_abstraction init recover abstr inited.

Axiom add_ok : forall v, proc_spec (add_spec v) (add v) recover abstr.

Axiom mean_ok : proc_spec mean_spec mean recover abstr.

Axiom recover_noop : rec_noop recover abstr no_crash.

Axiom add_ok : forall v, proc_spec (add_spec v) (add v) recover abstr.

Axiom mean_ok : proc_spec mean_spec mean recover abstr.

Axiom recover_noop : rec_noop recover abstr no_crash.

Hints to proof automation to apply the following proofs when "stepping"
through a procedure: e.g., if Coq has a add goal, it will try to apply
add_ok to resolve that goal. The implementation doesn't have to be concerned
with these hints.

Hint Resolve init_ok.

Hint Resolve add_ok.

Hint Resolve mean_ok.

Hint Resolve recover_noop.

End StatDbAPI.

Hint Resolve add_ok.

Hint Resolve mean_ok.

Hint Resolve recover_noop.

End StatDbAPI.