Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!udel!ee.udel.edu From: new@ee.udel.edu (Darren New) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: <50570@nigel.ee.udel.edu> Date: 12 Apr 91 20:47:40 GMT References: <1991Apr8.080931.23209@netcom.COM> <50097@nigel.ee.udel.edu> <1991Apr12.082128.11654@netcom.COM> Sender: usenet@ee.udel.edu Organization: University of Delaware Lines: 258 Nntp-Posting-Host: snow-white.ee.udel.edu In article <1991Apr12.082128.11654@netcom.COM> mrs@netcom.COM (Morgan Schweers) writes: > Really? It's not compilable, eh? Sounds real similar to BNF to me. Actually, it is a combination of CCP and ACT-One. (i.e., Calculus of Communicating Processes and equational data definitions.) >I accept that these are useful. You can't *PROGRAM* in them, but they >are useful as references. The point is that you have to write it in a >compilable language at some point. LOTOS can be compiled if you don't take advantge of (say) infinite numbers of processes or unlimited-size queues. I made another post explaining how to program in LOTOS. >your code has to go through a real compiler. That's where the work gets >done. By the programmer who does the implementation. He can't be >programming in a language that doesn't run, for obvious reasons. I disagree. "work" gets done all up and down the line. Work gets done by the person who gathers the specs, by the person who writes the C code, by the person who writes the C compiler and libraries, the testers, and so on. Formal languages help these people work together. > He can define the algorithms however he wants, as long as the >result is what comes off the spec. I understand this, as does (I >would imagine) all other programmers doing Real Work(tm). It's the >concept that I should program in a 'formalized' language that makes >me laugh. It's the idea that I should be worried that the language >ISN'T formally provable that makes me laugh. The informality of the language you use does not keep you from writing code in that language that works well. Rather, the formality helps you write better code faster. Analogy: assembler doesn't keep you from writing good code. C helps you write better code faster. >>You also have to know that it meets the customer's >>specifications. How do you do that with C? > ^^^^^^^^^^^^^^^^^^^^^^^^^^ (You test it.) You mean the customer tests it. You can't possibly know whether for subtle problems the program does what the customer wants because you may not know what the customer wants. In my experience, the *customer* doesn't know what the customer wants :-), and hence the "prototype" approach. > Who *IS* this Dan Bernstein guy? You're the second person to >mention him. He brings up good points, but he really really likes C. :-) > Yeah, 'more flexible than any compilable language', etc. Sheesh. >Do you ever get any work done? You write the specs for the >customer, no problem. I'll take it and make it work. Right? Right. Exactly. And the formalism makes me sure that I'm telling you what you are understanding. >>Then you have never seen a *real* formal specification and you >>shouldn't be claiming they are useless, since you've obviously never >>tried to use one. :-) > So enlighten me, mortal. I'll post references at the end of this article, since you are about the tenth person whose asked. >>you can't have a formal definition without math. LOTOS's definition > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ (Why?) Because "math" means "formal." (I think the word "math" comes from the name of the Arabic person who invented math, or something like that.) "Formal" means "based on the form". I.e., you can understand what is expressed by observing the "form" or "shape" of the argument without knowing what real-world things is relates to. :if P then Q :P :therefore Q I don't need to know what P or Q represent in the real world to know that this is "valid" in a formal sense. It may not be "true" if the things P and Q refer to don't match the formalism, but it is "valid" in my formalism. > You're right, to an extent. However, some projects are never >'finished' and cannot have a formal spec at the beginning because it >*MUST* change by the end, and would hamper more than help. Heh. The formalism would let you know exactly what parts of the project need to change when requirements change. >You've >probably never wortked on a project like that, so we really are talking >from two different points of view. Double heh. You haven't lived in "shifting spec" world until you've programmed life insurance software. It was always much easier when we got 1-2-3 spreadsheets than when we got papers with lots of scribbles and arrows. ESPECIALLY when changes were made, because we kept track in our source of which functions corresponded to which rows/columns. > Too true. I meant 'safe' as 'faithful' I suppose. Consider that >much of the code involved in the sort of work that I (and many other >programmers) do would fall under the heading of 'undefined' results. >(More specifically, platform-defined, or situation-defined.) "Platform defined" is not "undefined." Example platform defined: the open() call returns either a file handle or -1 if you reach a platform-defined limit. Example of undefined: the open() call returns a file handle. (Note no mention of error-behavior.) Which documentation would you rather use? >If the >sole purpose for the language is to have a language whose results >can be checked, as long as they are defined, then it makes no sense to >use it for things that will normally be site-defined. Does that make >sense? Sorry. No. :-( Whether a language if formally defined has little or nothing to do with site-defined behavior. Again, formal definitions are for inter-personal communication, not for checking results of a program against what *should* be the results of a program. >P.S. This has gotten *WAY* out of hand. We're talking about > messages 200+ lines in length, constantly. I love the discussion, > and am waiting for someone to define Formal Languages, but it's > getting a bit long. Will anyone settle for a pathetic, "We have > different opinions, because we do different jobs?" or is this > determined to be a continuing thread? I see no probelms as long as good information is being communicated. I think 200+ line posts are usually clearer and better thought-out than the "yes it is/no it isn't" posts we often get. As long as people keep posting, the discussion will continue. Below is the appropriate bits of my biblio file. The Brinksma tutorial is probably the easiest to understand. The international standard is of course the most complete. Even including the formal definitions of things like addition and subtraction, arabic decimal, hex, and binary numbers, flattening (i.e., scope resolution), and so on, the standard is still only about 50-100 pages. I would recommend the other tutorials (for Estelle and SDL) also. BTW, if you don't follow the "piano" examples in the tutorial, ignore them, learn LOTOS, and then go back and look at the piano examples. LOTOS is so different from most programming languages that trying to take an informal approach is more difficult than taking a formal approach. Let me know if there's anything else I can do for you. @techreport{Tenn88, title = "A Tutorial Introduction to Estelle", author = "R. Tenney", number = "88--1", institution = "Univerisity of Mass., Boston", month = jun, year = 1988 } @article{BB87, author = "T. Bolognesi and E. Brinksma", title = "Introduction to the ISO Specification Language LOTOS", journal = "Computer Networks and ISDN Systems", year = 1987, volume = 14, number = 1, pages = "25-60" } @article{BH89, author = "F. Belina and D. Hogrefe", title = "The CCITT Specification and Description Language SDL", journal = "Computer Networks and ISDN Systems", year = 1989, volume = 16, number = 4, pages = "311-341" } @manual{ISO8807, key = "ISO8807", title = "ISO International Standard 8807: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observat ional Behaviour", Xyear = 1989, organization = "Information Processing Systems - Open System Interconne ction" } @manual{GLOTOS, key = "ISO8807AD1", title = "ISO International Standard 8807: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observat ional Behaviour: Proposed Draft Addendum 1 (G-LOTOS)", Xyear = 1989, organization = "Information Processing Systems - Open System Interconne ction" } @book{BNT92, authors="Tommaso Bolognesi, Elie Najm and Paul Tilanus", title="G-LOTOS: a Graphical Language for Concurrent Systems", year="In preparation" } %NEW, 20 Jun 90, SCC @manual{ISO10167, key = "ISO10167", title = "ISO Draft International Standard 10167: Guidelines for the App lication of Estelle, LOTOS and SDL", Xnumber = "JCT1/SC21 N2549", organization = "Information Processing Systems - Open System Interconne ction", Xmonth = mar, Xyear = 1988 } @techreport{KSW88, author = "Steve King and Ib H. S\o{}rensen and James C.P. Woodcock", title = "Z: Grammar and Concrete and Abstract Syntaxes", institution = "Programming Research Group, Oxford University", address = "Oxford, UK", year = "1988", type = "Technical Monograph", number = "PRG-68", note = "ISBN 0902928503" } @techreport{Haye85, author = "Ian J. Hayes", title = "Specification Case Studies", type = "Technical Monograph", number = "PRG-46", institution = "Programming Research Group, Oxford University", address = "Oxford, UK", year = "1985", month = "July" } %NEW, 20 Jun 90 @article{THoo87, author = "G. T'Hooft", title = "Formal Description Techniques: Communication Tools for Data Co mmunication Specialists: Formal Specification and Im plementation of a File Transfer Protocol", journal = "Computer Networks and ISDN Systems", year = 1987, volume = 14, number = 1, pages = "311--321" } -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, FDTs ----- +=+=+ My time is very valuable, but unfortunately only to me +=+=+