This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: "Documentation by paper"
- From: dewar at gnat dot com (Robert Dewar)
- To: Joe dot Buck at synopsys dot com, jamie at shareable dot org
- Cc: asutton at cs dot kent dot edu, dewar at gnat dot com, gcc at gcc dot gnu dot org,kenner at vlsi1 dot ultra dot nyu dot edu, law at redhat dot com
- Date: Mon, 2 Feb 2004 12:19:03 -0500 (EST)
- Subject: Re: "Documentation by paper"
> I would add that a real spec tells you what the function _does_ and
> sometimes how to use it, in addition to pre/postconditions :)
It also might have *some* details of the implementation if they are
important to its use, e.g. knowing whether a sort is nlogn or n**2.
Of course sufficiently powerful pre and post conditions would be able
to describe what a function does, but if these conditions are written
in a low level language without set comprehension and quantifiers, this
can be impractical in practice.