PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_specifications

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

Global Imports

From Coq Require Import SetoidClass.

Local Imports

From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

Proof of self-stabilization and specification
Proof of a complexity bound in steps
Proof that this complexity bound is exact (by building a worst case prefix of execution)

Dijkstra's Token Ring Specifications

/contains:/ Token Circulation Specification: A unique token always eventually passes through each node.

The specification is a property on an execution and contains

a function that checks at each node whether the node holds a token
a predicate which is satisfied when there is at most one token in the network
a predicate which checks that every node always eventually holds a token

Section Token_Circulation_Spec.

  Context {Chans: Channels}
          {Net: Network}
          {Algo: Algorithm}.

  Definition Token_Circulation_Spec (e: Exec): Prop :=
    exists (Token: Env -> Node -> Prop),

      Always (fun e_ => forall n1 n2,
                  Token (s_hd e_) n1 ->
                  Token (s_hd e_) n2 -> n1 == n2) e
      /\

      forall (n: Node),
        Always (Eventually (fun e_ => Token (s_hd e_) n)) e.

End Token_Circulation_Spec.

Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature_scope.