Partial order

The notion of partial order provides a foundation for verification of the priority-inversion freedom and the deadlock freedom of multitask scheduling systems. In this section, we introduce modules to represent strict partial orders.

Let S be a set and R be a binary relation on S. Then R is called a strict partial order if R satisfies the following condition.

• irreflexivity： ∀x∈S・¬（x R x）
• asymmetricity： ∀x,y∈S・¬（x R y ∧ y R x)
• transitivity： ∀x,y,z∈S・（x R y ∧ y R z）⇒ x R z

Where x R y means that the pair <x,y> is belongs to the relation R. Please notice that irreflexivity is equivalent to asymmetricity under transitivity, i.e., * Asymmetricity can be derived from irreflexivity and transitivity * Irreflexivity can be derived from asymmetricity and transitivity

However, the module introduced in this section which represents strict partial orders declares these three conditions. From now, the word "partial order" means strict partial order.

RELATION

First of all, we have to declare a module which declares a sort of binary relations.

#!python

module RELATION
(
  X :: TRIV
)
{
  imports
  {
    pr(PROP)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Relation ]
    op ___ : Elt Relation Elt -> Prop
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : Relation
-- substitution
    eq deducible((X = Y),(X R Z) |- (Y R Z)) = true .
    eq deducible((X = Y),(Z R X) |- (Z R Y)) = true .
  }
}

IRREFLEXIVE

The module IRREFLEXIVE denotes irreflexive binary relations.

#!python
module IRREFLEXIVE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Irreflexive < Relation ]
  }
  axioms
  {
    vars X : Elt
    vars R : Irreflexive
-- irreflexivity
    eq deducible((X R X) |- nil) = true .
    eq deducible(nil |- (neg X R X)) = true .
  }
}

ASYMMETRIC

The module ASYMMETRIC denotes asymmetric binary relations.

#!python

module ASYMMETRIC
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Asymmetric < Relation ]
  }
  axioms
  {
    vars X Y : Elt
    vars R : Asymmetric
-- asymmetricity
    eq deducible((X R Y),(Y R X) |- nil) = true .
  }
}

The above module declares the sort Asymmetric as a subsort of Relation which satisfies the asymmetricity.

TRANSITIVE

The module TRANSITIVE denotes transitive binary relations.

#!python
module TRANSITIVE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Transitive < Relation ]
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : Transitive
-- transitivity
    eq deducible((X R Y),(Y R Z) |- X R Z) = true .
  }
}

The above module declares the sort Transitive as a subsort of Relation which satisfies the transitivity.

PARTIALORDER

We declare the module PARTIALORDER which declares the sort PartialOrder which is a subsort of Irreflexive, Asymmetric and Transitive.

#!python

module PARTIALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R)
)
{
  signature
  {
    [ PartialOrder < Irreflexive Asymmetric Transitive ]
  }
}

By the above subsorting, it is assumed that a member of PartialOrder satisfies the irreflexivity, the assymetricity and the transitivity.

TOTALORDER

Moreover, we declare the module TOTALORDER which declares the sort TotalOrder which is a subsort of PartialOrder.

#!python

module TOTALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T)
)
{
  signature
  {
    [ TotalOrder < PartialOrder ]
  }
  axioms
  {
    vars X Y : Elt
    vars R : TotalOrder
    eq deducible(nil |- (X = Y),(X R Y),(Y R X)) = true .
  }
}