[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

How can we extend type bool with a "bottom" element?


we have a question concerning extending the predefined boolean type with
an additional "bottom" element. 
Extending e.g. integers with a bottom element is not difficult since
there exist supertypes of the integers (e.g rationals); one can just 

  rat_nonint: TYPE = {x: rat | FORALL (y: int): x /= y} CONTAINING 2/3
  bt: rat_nonint
  gen_int: TYPE = {x: rat | x = bt OR integer_pred(x)}.

Then bt is the designated bottom element. The most important thing in this
context is  that we can still use all functions which return integer
values in assignments to gen_int variables. Exactly the same we would like
to do with the extended boolean type that we are looking for; it is
important that we can still use e.g comparison functions on integers (
which return a boolean value) in assignments to gen_bool variables. Thus
we can not simply use an enumeration type. It seems that there does not
exist a union type constructor in PVS so how can we define the gen_bool's?

Thanks for your help
Ofer and Michael

Ofer Shtrichman
E-mail: ofers@wisdom.weizmann.ac.il
The Weizmann Institute of Science
Department of Applied Mathematics & Computer Science, Rehovot 76100,
Tel. (W) (temporary) : (972) 08-9342856
Tel. (H)             : (972) 03-5713880