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.