Go to the first, previous, next, last section, table of contents.


11.5 void

Although many programmers do not think of void as a type, and those that do often think of it as a type with no values, the type void is properly modeled as a type with exactly one value. This is modeled by the following trait in Larch/C++. (See section 6.11 Exceptions for the trait NoInformation.)

% @(#) $Id: void.lsl,v 1.2 1995/11/13 16:24:07 leavens Exp $
void : trait
  includes NoInformation(void, theVoid for it)
  implies
    \forall x, y: void
       x == theVoid;
       x == y;

One reason to have a value of the void type is to have a model for the abstract value of a "void pointer", that is a pointer of type void*. The abstract value of an object pointed to by such a pointer exists, but has no information content. Therefore the abstract value of such an object is theVoid, which is the only abstract value of type void.


Go to the first, previous, next, last section, table of contents.