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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,14f7200925acb579 X-Google-Attributes: gid103376,public From: Florian Weimer Subject: Re: No Go To's Forever! Date: 2000/03/29 Message-ID: <874s9p7jwi.fsf@deneb.cygnus.argh.org>#1/1 X-Deja-AN: 603963699 References: <8bbsc6$aes$1@nnrp1.deja.com> <8bdbof$t19$1@nnrp1.deja.com> <38E1F6D5.8303903C@dowie-cs.demon.co.uk> Mail-Copies-To: never Content-Type: text/plain; charset=us-ascii X-Complaints-To: abuse@cygnus.argh.org X-Trace: deneb.cygnus.argh.org 954351741 6702 192.168.1.2 (29 Mar 2000 17:42:21 GMT) Organization: Penguin on board User-Agent: Gnus/5.0804 (Gnus v5.8.4) Emacs/20.6 Mime-Version: 1.0 Reply-To: Florian Weimer NNTP-Posting-Date: 29 Mar 2000 17:42:21 GMT Newsgroups: comp.lang.ada Date: 2000-03-29T17:42:21+00:00 List-Id: Martin Dowie writes: > one of the reasons I had always been told for avoiding using gotos, was > that it makes a program unprovable. a) was this true; No. > and if so, b) is this still true? No. (Why should it have changed, BTW? I wouldn't call something unprovable unless it has been proven to be unprovable.) One of the standard textbooks in computer science uses gotos quite heavily, and it contains correctness proofs. Although the proofs are not "formal", and neither is the algorithm description, they are more substantial than the "formal" proofs which I've seen at the local CS department. BTW: What does "formal program verification" mean in practice? I was told that it must involve quantifiers and other fancy stuff. Is this true, or are rigid, but non-formal proofs considered sufficient (i.e. proofs whose formalization is easy, but tedious work, and which would result in proofs nobody could understand). After attending some CS courses, I should probably know it, but our formal program verification exercises where quite a nightmare (for example, we should prove the correctness of an implementation without having the specification).