Re: Type System as Design Tool [Was: We do not use C++ exceptions]

From:

David Abrahams <dave@boostpro.com>

Newsgroups:

comp.lang.c++.moderated

Date:

Thu, 19 Feb 2009 12:55:31 CST

Message-ID:

<87r61uwe6m.fsf@mcbain.luannocracy.com>

on Thu Feb 19 2009, Thant Tessman <thant.tessman-AT-gmail.com> wrote:

Andrei Alexandrescu wrote:

[...]

So what's needed now is some amount of qualifying of your initial
statement. You now claim that this:

fun pop [] = []
| pop (_ :: rest) = rest

obviates the need for design by contract because it forces you to write
what happens when the stack is empty. But the contract is _there_, and
it states that pop from an empty stack returns empty. People will still
attempt to pop from empty stacks, and that will still compile and run.
So the type system hasn't help you zilch in designing a Stack type that
doesn't need a contract. [...]

So a 'contract' is what a programmer has decided to do in the case that
a stack is empty?

If you want to know what 'contract' means in this context, why don't you
start here: http://en.wikipedia.org/wiki/Design_by_contract

   Design by Contract (DbC) or Programming by Contract is an approach to
   designing computer software. It prescribes that software designers
   should define formal, precise and verifiable interface specifications
   for software components based upon the theory of abstract data types
   and the conceptual metaphor of a business contract. Thus, it can be
   considered as an evolution of the abstract data type theory.

   ...

Regards,

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com

      [ See http://www.gotw.ca/resources/clcm.htm for info about ]
      [ comp.lang.c++.moderated. First time posters: Do this! ]