Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!rutgers!cmcl2!lanl!opus!ted From: ted@nmsu.edu (Ted Dunning) Newsgroups: comp.sw.components Subject: Re: Ada 9X objectives Message-ID: Date: 4 Oct 89 15:33:50 GMT References: <6658@hubcap.clemson.edu> <6661@hubcap.clemson.edu> <935@scaup.cl.cam.ac.uk> Sender: news@nmsu.edu Organization: NMSU Computer Science Lines: 39 In-reply-to: scc@cl.cam.ac.uk's message of 4 Oct 89 01:08:22 GMT In article <935@scaup.cl.cam.ac.uk> scc@cl.cam.ac.uk (Stephen Crawley) writes: Bill Wolfe replies: > Finally, formal verification is a > major goal of the software engineering community, and Ada was designed > to support it to as great an extent as possible. For example, the > use of the termination model of exception handling was (at least in > part) motivated by formal verification considerations. Excuse me while I laugh ... Verifying ADA 83 is a fundamentally intractible problem for any number of reasons. I don't believe anyone has even managed to formally define the semantics of ADA 83! Maybe some members of the ADA design team did have verification in their minds ... but others didn't, and the others won the day. compare this situation to that of scheme where the formal semantics of the language _have_ been defined, and they are concise enough to fit on a couple of pages. in fact, they are so simple and straightforward that the formal semantics can be used in an undergraduate computer science class. even more interesting, these formal semantics were automatically derived from a running scheme program which provides an executable model of the semantics. this allows much simpler testing of the semantics than just writing down the equations and having people stare at them. -- ted@nmsu.edu remember, when extensions and subsets are outlawed, only outlaws will have extensions or subsets