markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/14/90)
In article <25711@cup.portal.com> mmm@cup.portal.com (Mark Robert Thorson) writes: >There was an excellent article about 10 years ago in CACM on this. >I believe the title was "The Social Process and Proofs of Program >Correctness". This article marked the death of program verification; I must've missed the boat: I always prove my programs correct. Pathologies in provability (which are theoretically guaranteed) almost always indicate flaws in design. Therefore undecibeability is actually an AID in program verification, not an obstacle. Programs in even languages like C, Pascal can be manipulated via a set of (complete) algebraic rules -- which form a foundation for the semantics of the language in question. I use such rules all the time. >... from that point on the "conventional wisdom" was that program >verification was a dead-end for research. In retrospect, it's hard >hard to see why this wasn't obvious from the very beginning. Oh, the irony...
larry@csccat.UUCP (Larry Spence) (01/16/90)
In article <1888@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >I must've missed the boat: I always prove my programs correct. Could you give us some examples? What is the largest program you have proven correct? How long did the design and proof process take? Are these programs applications that are used by others, or academic exercises? >Programs in even languages like C, Pascal can be manipulated via a set of >(complete) algebraic rules -- which form a foundation for the semantics >of the language in question. Can you give us pointers to literature (or examples of your own) where a real-world C program of more than a few dozen lines (i.e., including side- effects from pointers, aliasing, etc.) is manipulated in a non-trivial manner (you get to define "non-trivial") via such a set of rules? Do any of your "correct" programs use floating point arithmetic (or fixed- point, for that matter)? Can such programs be proven correct? Would you maintain that real-world applications other than those which MUST be correct at any cost (e.g., space missions, medical apps) SHOULD be proven correct? Do you think that this would be cost-effective? -- Larry Spence larry@csccat ...{texbell,texsun,attctc}!csccat!larry