Wiki

Basic modules

In this section, we introduce some basic modules used in the formal description of the OSEK/VDX specification.

NIL

The module NIL is used to represent empty structures including an empty list, an empty set, etc.

#!cafeobj
module NIL
{
  signature
  {
    [Nil]
    op nil : -> Nil
  }
}

PROP

The module PROP is to represent propositions. In this module, we introduce the sort Prop as a supersort of Bool to prevent the CafeOBJ processor from reducing terms beyond our intention. This module declares the following operations.

negation (neg_)
disjunction（\/）
conjunction（_/_）
implication（=>）
equivalence（<=>）

#!cafeobj
module PROP
{
  signature
  {
    [ Bool < Prop ]
    op _/\_ : Prop Prop -> Prop { assoc comm prec: 55 }
    op _\/_ : Prop Prop -> Prop { assoc comm prec: 59 }
    op neg_ : Prop -> Prop { prec: 53 }
    op _=>_ : Prop Prop -> Prop
    op _<=>_ : Prop Prop -> Prop
  }
  axioms
  {
    vars P Q R : Prop
    eq false /\ P = false .
    eq true /\ P = P .
    eq P /\ P = P .
    eq true \/ P = true .
    eq false \/ P = P .
    eq P \/ P = P .
    eq neg true = false .
    eq neg false = true .
    eq neg neg P = P .
--  eq neg(P \/ Q) = (neg P) /\ (neg Q) .
--  eq neg(P /\ Q) = (neg P) \/ (neg Q) .
    eq P => true = true .
    eq P => false = neg(P) .
    eq true => P = P .
    eq false => P = true .
    eq P => P = true .
    eq P <=> Q = (P => Q) /\ (Q => P) .
  }
}

NUMBER

The module NUMBER is to represent Peano arithmetic. This module declares the following operations.

zero (0)
successor（s_）

#!cafeobj
module NUMBER
{
  signature
  {
    [ Number ]
    op 0 : -> Number
    op s_ : Number -> Number
  }
}

SET

The module SET is a parameterized module to represent a set of elements of the sort declared in the module which is given to instantiate SET. This module declares the following operations.

set union（,）
membership relation（@）
set difference（__）
cardinal（#）

#!cafeobj
module SET
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    ex(PROP)
    pr(NUMBER)
--  pr(NAT)
  }
  signature
  {
    [ Nil Elt < Set ]
    op _,_ : Set Set -> Set { assoc comm idem id: nil }
    op _@_ : Elt Set -> Prop
    op _\_ : Set Set -> Set
--  op # : Set -> Nat
    op # : Set -> Number
  }
  axioms {
    vars X Y : Elt
    vars S T : Set
    eq (S,X = nil) = false .
    eq X @ nil = false .
    cq X @ (Y,S) = true
       if (X = Y) .
    cq X @ (Y,S) = X @ S
       if neg(X = Y) .
    eq nil \ S = nil .
    eq S \ nil = S .
    eq S \ (X,T) = (S \ X) \ T .
    eq (S,X) \ X = S .
    cq (S,Y) \ X = S \ X
       if (neg X = Y) .
    eq #(nil) = 0 .
    cq #(X,S) = s(#(S))
       if neg(X @ S) .
    cq #(X,S) = #(S)
       if (X @ S) .
  }
}

LIST

The module LIST is also a parameterized module to declare a list of elements of the sort which is declared in the given module. In this module, the following operations are declared.

list concatenation（;）
membership relation（?）
removal of an element （-）
the number of elements（occur）
position of a given element (position)

#!cafeobj

module LIST
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    pr(PROP)
    ex(NUMBER)
--  pr(NAT)
  }
  signature
  {
    [ Nil Elt < List ]
    op _;_ : List List -> List { assoc id: nil }
    op _?_ : Elt List -> Prop
    op _-_ : List Elt -> List
--  op occur : List Elt -> Nat
    op occur : List Elt -> Number
--  op front : List Elt -> List
--  op member : List -> Set
    op position : List Elt -> Number
  }
  axioms
  {
    vars X Y : Elt
    vars L F : List
    eq X ? nil =  false .
    cq X ? (Y;L) =  true
       if X = Y .
    cq X ? (Y;L) =  X ? L
       if neg(X = Y) .
    eq nil - X = nil .
    eq (X;L) - X = L .
    cq (Y;L) - X = Y;(L - X)
       if neg(X = Y) .
    eq occur(nil,X) = 0 .
--  eq occur((X;L),X) = occur(L,X) + 1 .
    eq occur((X;L),X) = s(occur(L,X)) .
    cq occur((Y;L),X) = occur(L,X)
       if neg(X = Y) .
--  eq front(nil,X) = nil .
--  eq front((X;L),X) = nil .
--  cq front((Y;L),X) = Y;(front(L,X))
--     if neg(X = Y) .
--  eq X ? front(L,X) = false .
--  eq member(nil) = nil .
--  cq member(X;L) = X,member(L)
--     if neg(X ? L) .
--  cq member(X;L) = member(L)
--     if (X ? L) .
    eq position((X;L),X) = 0 .
    cq position((X;L),Y) = s(position(L,X))
       if neg(X = Y) .
  }
}

BAG

The module BAG is a parameterized module to represent a multiset of elements of the sort declared in a given module. This module declares the following operations.

multiset union（|）
membership relation（in）
multiset difference（sub）
cardinal（#）
the number of a given element（bag）

#!cafeobj
module BAG
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    ex(PROP)
    pr(NUMBER)
--  pr(NAT)
  }
  signature
  {
    [ Nil Elt < Bag ]
    op _|_ : Bag Bag -> Bag { assoc comm id: nil }
    op _in_ : Elt Bag -> Prop
    op _sub_ : Bag Bag -> Bag
--  op # : Bag -> Nat
    op # : Bag -> Number
--  op bag : Bag Elt -> Nat
    op bag : Bag Elt -> Number
  }
  axioms {
    vars X Y : Elt
    vars S T : Bag
    eq (S | X = nil) = false .
    eq X in nil = false .
    cq X in (Y | S) = true
       if (X = Y) .
    cq X in (Y | S) = X in S
       if neg(X = Y) .
    eq nil sub S = nil .
    eq S sub nil = S .
    eq S sub (X | T) = (S sub X) sub T .
    eq (S | X) sub X = S .
    cq (S | Y) sub X = S sub X
       if (neg X = Y) .
    eq #(nil) = 0 .
--  eq #(X | S) = 1 + #(S) .
    eq #(X | S) = s(#(S)) .
    eq bag(nil,X) = 0 .
    cq bag((Y | S),X) = bag(S,X)
       if (neg X = Y) .
--  cq bag((Y | S),X) = 1 + bag(S,X)
    cq bag((Y | S),X) = s(bag(S,X))
       if (X = Y) .
  }
}