kn-boolean.gas - A specification of the abstract datatype boolean.

Lecture 1 - slide 10 : 22 Program 3

Type boolean []
  declare
    constructors
      true() -> boolean;
      false() -> boolean;
    others
      not (boolean) -> boolean;
      and (boolean, boolean) -> boolean;
      or (boolean, boolean) -> boolean;
      implies (boolean, boolean) -> boolean; 
  for all
      b, c in boolean;
    let
      not(true()) = false();
      not(false()) = true();
      and(true(),b) = b;
      and(false(),b) = false();
      or(true(),b) = true();
      or(false(),b) = b;
      implies(b,c) = or(not(b),c);
    end
end boolean.