Programming Languages (CS302 2005S)

Gries, Chapters 0 and 1

Gries, David (1998). The Science of Programming. New York, NY: Springer-Verlag. ISBN: 0-387-96480-0. Chapter 0: Why Use Logic? Why Prove Programs Correct? (pp. 1-6) and Chapter1 (pp. 7-18).

The book states that the or operation denotes "inclusive or" as opposed to "exclusive or". What is the formal definition for the "exclusive or" and is there a way to represent it, or is there no need to?

It seems like the method of strictly asserting preconditions and postconditions can only work when exact pre and postconditions are known. What if you're dealing with a chaotic system of some sort where there's no succinct way to describe the post condition, or possibly even the intermediate steps? Can correctness be proven for such a program in the way Gries describes? (On larger projects, too, even if you know that each individual component, if given the correct input, is correct, it seems like situations would arise that, to ensure that each component gets the correct input would require keeping so many different rules and results in your head that it seems beyond the scope of human intelligence and bugs would still creep into the framework.)

Considering the Boolean system used to prove whether a program is correct or not, how can one be sure a program is correct if the input or output or the program is not necessarily known, is obscure, or has not been determined yet?

it's not technically in the reading but it it referenced. In Appendix I on BNF on page 306 i don't fully understand the notation =>*. It is sone kind of reassignment but i'm not exactly sure how it functions.

Would Gries consider all conditional statements in the English language to be propositions?

His propositions are over Boolean variables, so probably not.

Is it possible to show that a proposition is a tautology in polynomial time? It seems similar to the SAT problem.

Yes, the problems are similar. I believe general proof of tautologies is not polynomial.

Gries asserts that programs developed hand-in-hand with there correctness proofs will take significantly less time to develop and debug. Considering the example presented in chapter 0, Gries' idea of standalone programming appears to significantly lacking in the design phase. Do you think proving the correctness of a program will improve the programmers' productivity significantly over only implementing proper programming design?

"If we had reason to believe a conjecture, it is unlikely that its converse is true." page 15. The truth value of a conjecture is not determined by the truth value of its converse, or vice versa. Gries' argument that (not e) being a tautology disproves e being a tautology is correct, however, I do not think the relationship is that of a statement and its converse.

In the world of Boolean logic, the truth of a conjecture must be the opposite of its converse.

Gries mentions that the study of program correctness proofs can lead to the development of programs free of errors. Of course, human mistakes are inevitable. So, why learn this late about program correctness? Why not approaching this issue early in the curriculum?

We now include Gries in CSC 201, which should be most students' third of forth course in the major.

In chapter 1, section 1.2, Gries explains the concept of the Boolean operator "implication". Please explain how implication works.

Not so much about the propositions.. but why are the nonterminals factor, term, and expression used here and in grammars for numerical expression? I see a correlation: AND is like * and OR is like + based on the way 0 (False) behaves ( 0*anything=0 while "False AND anything = False") ... are there other aspects to this? Where does this terminology come from? What else could be a thought of as a "term" versus a "factor"?

As far as I know, these are convenient terms someone came up with when disambiguating a grammar and they've stuck.

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Wed Mar 2 11:39:32 2005.
The source to the document was last modified on Thu Feb 3 21:05:23 2005.
This document may be found at

You may wish to validate this document's HTML ; Valid CSS! ; Check with Bobby

Samuel A. Rebelsky,