Although many programmers do not think of
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
% @(#) $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
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
which is the only abstract value of type
Go to the first, previous, next, last section, table of contents.