From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-01-11 06:19:01 PST Path: archiver1.google.com!news2.google.com!fu-berlin.de!news-FFM2.ecrc.net!news.net.uni-c.dk!sunsite.dk!newsfeed1.uni2.dk!news.get2net.dk.POSTED!53ab2750!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <86k73ysqn6.fsf@huldreheim.huldreskog.no> From: Mark Lorenzen Message-ID: User-Agent: Gnus/5.1002 (Gnus v5.10.2) Emacs/21.3 (gnu/linux) Cancel-Lock: sha1:+FRB7HKk5BQNbnKeGYjAHCYHfI4= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 09 Jan 2004 11:11:26 +0100 NNTP-Posting-Host: 62.84.221.216 X-Complaints-To: abuse@colt-telecom.dk X-Trace: news.get2net.dk 1073830740 62.84.221.216 (Sun, 11 Jan 2004 15:19:00 CET) NNTP-Posting-Date: Sun, 11 Jan 2004 15:19:00 CET Organization: Colt Telecom Kunde Xref: archiver1.google.com comp.lang.ada:4330 Date: 2004-01-09T11:11:26+01:00 List-Id: Leif Roar Moldskred writes: > tmoran@acm.org writes: > >> Specification: the program will print, on January 30, 2004, the name >> of the President of the United States on January 30, 2005. >> That wasn't a hard spec to write - I await your implementation. ;) > > In pseudo-code: > > PRINT ( "There will be no President of the United States on January 30th, 2005" ) > FOR EACH name in set_of_candidates_for_president DO > PRINT( "The President of the United States on January 30th, 2005 will be " ) > PRINT( name ) > DONE > > Now, if your specification had explicitly stated that the program should print > out _only_ the name of the person who will be president of the United States > on January 30th, 2005, it would have been harder. > > -- > Leif Roar Moldskred > Got Sfik? Beautiful example showing that the "Print_President_Name" function was underspecified. In this case the original specification made implicit use of some knowledge in the domain. This is often (allways?) the case with texual descriptions and specifications and is probably one of the causes that it is so difficult to write formal specifications. The math itselt is not difficult (at least not on the "user level"), but remembering all the necessary statements about the domain and the problem is. - Mark Lorenzen