Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use

`Ctrl+↑``Ctrl+↓`to navigate,`Ctrl+🖱️`to focus.`Require Import POCS.`

# 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

`Definition State := list nat.`

```
Definition inited (s : State) : Prop :=
s = nil.
```

## 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

`Module Type StatDbAPI.`

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.

The abstraction relation between spec and code state

Axiom abstr : Abstraction 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_wipe : rec_wipe 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 : core. Hint Resolve add_ok : core. Hint Resolve mean_ok : core. Hint Resolve recover_wipe : core. End StatDbAPI.