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.
;
Check with Bobby