PADEC - Coq Library

Library Padec.BFS.BFS_specification_proved

*Certified Round Complexity of Self-Stabilizing Algorithms*

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Lia.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import BFS_algo.
From Padec Require Import BFS_common.
From Padec Require Import BFS_specification.
From Padec Require Import BFS_correctness.
From Padec Require Import BFS_rounds.
From Padec Require Import Rounds.

Open Scope nat_scope.
Set Implicit Arguments.

BFS: Proof of self-stabilization and specification

Specifications Proved

/contains:/ Proof that the algorithm is self-stabilizing wrt BFS construction (the algorithm is silent).

/assumes:/ G = (V, E) connected, rooted (r), semi-anonymous, Some constant D >= Diameter of G Weakly fair daemon

Closure: silent algorithm
Convergence: The result is direct from complexity.
Specification: BFS construction

Section BFS_spec_proved.

  Context {Chans: Channels}
          {Net: Network}
          {Graph_assumption: BFS_Assume}
          {Graph_network_assumption: Graph_Network_matching}
          {D_Assumption: BFS_D}.

  Existing Instance G_compat.

  Notation Algo := (BFS_algo D).
  Notation Env := (Env (Net := Net) (Algo := Algo)).

  Existing Instance BFS_RO_assumption.

Convergence: eventually a legitimate configuration is

reached Obtained from round complexity

Lemma BFS_convergence:
convergence BFS_RO_assumption weakly_fair terminal.

Specification

  Theorem BFS_self_stab_prop:
    self_stabilization
      BFS_RO_assumption weakly_fair
      (only_one (BFS_Spanning_Tree_spec Root Par_Rel)).

End BFS_spec_proved.

Unset Implicit Arguments.
Close Scope nat_scope.