COMP1600讲解、辅导Java编程、讲解c/c++，Python语言
- 首页 >> Python编程 COMP1600/COMP6260
(Foundations of Computation)
Writing Period: 3 hours duration
Study Period: 15 minutes duration
Permitted Materials: One A4 page with hand-written notes on both sides
Answer ALL questions
Total marks: 100
The questions are followed by labelled blank spaces into which your answers are to be written.
Additional answer panels are provided (at the end of the paper) should you wish to use more
space for an answer than is provided in the associated labelled panels. If you use an additional
panel, be sure to indicate clearly the question and part to which it is linked.
The following spaces are for use by the examiners.
Q1 (Logic) Q2 (ND) Q3 (SI) Q4 (HL) Q5 (FSA) Q6 (CFL)
Q7 (TM) Total
COMP1600/COMP6260 (Foundations of Computation) Page 1 of 27
QUESTION 1 [14 marks] Logic
Recall that two formulae are equivalent if they have have the same truth values for all variable
assignments, and consider the following set of formulae:
• (p ∧ q) ∨ (¬p ∧ ¬q)
• ¬p ∨ q
• (p ∨ ¬q) ∧ (q ∨ ¬p)
• ¬(p ∨ q)
• (q ∧ p) ∨ ¬p
(a) Identify two formulae in the above set of formulae that are equivalent, and demonstrate
their equivalence by means of a truth table.
QUESTION 1(a) [4 marks]
(b) Identify two formulae in the above set of formulae that are not equivalent, and demonstrate
the fact that they are not equivalent by a variable assignment.
QUESTION 1(b) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 2 of 27
(c) State whether the following formulae are true or false where x, y and z range over the
integers, and justify your answer briefly.
(1). ∀ x ∃ y(2x − y) = 0
(2). ∃ x ∀ y(2x − y) = 0
(3). ∀ x ∃ y(x − 2y) = 0
QUESTION 1(c) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 3 of 27
QUESTION 2 [16 marks] Natural Deduction
The following questions ask for proofs using natural deduction. Present your proofs in the Fitch
style as used in lectures. You may only use the introduction and elimination rules given in
Appendix 1. Number each line and include justifications for each step in your proofs.
(a) Give a natural deduction proof of the formula p ∨ (p → q). In this proof, you may use the
law of excluded middle (LEM) p ∨ ¬p in addition to the rules provided in the appendix.
That is, you may state p ∨ ¬p at any line in the proof, where p can stand for an arbitrary
formula, and justify this by (LEM).
QUESTION 2(a) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 4 of 27
(b) Give a natural deduction proof of the rule
∃ xP(x) ∧ ∀ x ∀ y(R(x, y) → P(y))
∃ x ∀ y(R(x, y) → P(y))
using only the rules in the appendix.
QUESTION 2(b) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 5 of 27
QUESTION 3 [16 marks] Structural Induction
(a) Consider the function subl that computes the list of sub-lists of a given list:
subl :: [a] -> [[a]]
subl [] = [[]] -- S1
subl (x:xs) = (subl xs) ++ map (pref x) (subl xs) -- S2
where the functions map, pref and ++ are given by:
map :: (a -> b) -> [a] -> [b]
map f [] = [] -- M1
map f (x:xs) = (f x):(map f xs) -- M2
pref :: a -> [a] -> [a]
pref x l = x:l -- P
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- A1
(x:xs) ++ ys = x : (xs ++ ys) -- A2
Show, using structural induction, that
length (subs l) = 2length l
for all lists l of type a.
Here, we assume the standard definition of the length function
length [] = 0 -- L1
length (x:xs) = 1 + length xs -- L2
and you may use the fact that map preserves length, and the fact that length is compatible
with concatenation, that is the equations
length (map f xs) = length xs -- LM
length (xs ++ ys) = length xs + length ys -- LA
in your proof, with justification as indicated.
In all proofs indicate the justification (eg, the line of a definition used) for each step.
COMP1600/COMP6260 (Foundations of Computation) Page 6 of 27
(i) State and prove the base case.
QUESTION 3(a)(i) [2 marks]
(ii) State the inductive hypothesis.
QUESTION 3(a)(ii) [1 mark]
(iii) State and prove the step case goal.
QUESTION 3(a)(iii) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 7 of 27
(b) Give an inductive proof the fact that left folding is compatible with list concatenation.
Consider the following definition of left folding:
foldl :: :: (b -> a -> b) -> b -> [a] -> b
foldl f z [] = z -- F1
foldl f z (x:xs) = foldl f (f z x) xs -- F2
and consider a fixed function f (of type b -> a -> b) and a fixed list ys (of elements of
type b) and show that
P(xs) ≡ ∀ z (foldl f z (xs ++ ys) = foldl f (foldl f z xs) ys)
holds for all lists xs (of elements of type a).
(i) State and prove the base case goal
QUESTION 3(b)(i) [2 marks]
(ii) State the inductive hypothesis
QUESTION 3(b)(ii) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 8 of 27
(iii) State and prove the step case goal.
QUESTION 3(b)(iii) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 9 of 27
QUESTION 4 [16 marks] Hoare Logic
(a) Specify a precondition P and a postcondition Q such that the Hoare-Triple {P} S {Q}
holds precisely for all programs S that never terminate.
QUESTION 4(a) [2 marks]
(b) The following piece of code is called Rem
r := x;
q := 0;
while (r >= n)
r := r - n;
q := q + 1
and computes two numbers, q and r, where
• q is the integer quotient of x by n
• r is the remainder of the division of x by n.
We wish to use Hoare Logic (Appendix 3) to show that:
{True} Rem {x = n ∗ q + r}
In the questions below (and your answers), we may refer to the loop code as Loop, the
body of the loop (i.e. r:-r-n;q:=q+1) as Body, and the initialisation assignments (i.e.
r:=x;q:=0) as Init.
(i) Given the desired postcondition {x = n ∗ q + r}, what is a suitable invariant I for
Loop?
QUESTION 4(b)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 10 of 27
(ii) Prove that your answer to the previous question is indeed a loop invariant. That is,
if we call your invariant I, show that {I} Body {I}. Be sure to properly justify each
step of your proof.
QUESTION 4(b)(ii) [3 marks]
(iii) Using the previous result and some more proof steps show that
{True} Rem {x = n ∗ q + r}
Be sure to properly justify each step of your proof.
QUESTION 4(b)(iii) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 11 of 27
(iv) Explain why the corresponding Hoare-triple for total correctness, that is
[True]Rem[x = n ∗ q + r]
is not valid by giving a counter-example that shows that the triple above does not
hold in general.
QUESTION 4(b)(iv) [2 marks]
(v) Identify a precondition P such that the Hoare triple
[P]Rem[x = n ∗ q + r]
is valid. Explain why the Hoare-triple now holds (no formal proof in Hoare Logic
required).
QUESTION 4(b)(v) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 12 of 27
QUESTION 5 [13 marks] Finite State Automata
(a) Design a Finite State Automaton that recognises the language of all strings over the alphabet
Σ = {a, b, c} where both the string ’abc’ and the string ’cba’ occurs as a substring.
Here, a string s is a substring of a string w if w can be written as w1sw2.
QUESTION 5(a) [3 marks]
(b) Is your Finite State Automaton (above) deterministic or non-deterministic? Explain.
QUESTION 5(b) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 13 of 27
(c) What language is recognised by the following Finite State Automaton?
Describe the language in English, and give a regular expression defining the language.
QUESTION 5(c) [3 marks]
(d) Consider the statement
∀ w ∈ Σ
∗
. N
∗
(q2,w) = q2
Express this property in English. Why might it be relevant?
QUESTION 5(d) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 14 of 27
(e) For the Finite State Automaton above, prove that
∀ n ∈ N . N
∗
(q1,(aa)
n
) = q1
and hence, or otherwise, conlude that
∀ n ∈ N . N
∗
(q0,(aa)
n+1) = q1
QUESTION 5(e) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 15 of 27
QUESTION 6 [13 marks] Context-Free Grammars
(a) Design a push-down automaton that recongnises precisely the language
{a
m
b
n
| n > m > 0}
QUESTION 6(a) [4 marks]
(b) Is your automaton deterministic, or non-deterministic? Briefly justify your answer.
QUESTION 6(b) [1 mark]
(c) Demonstrate, using the pigeon hole principle or otherwise, that the language given above
is not regular.
QUESTION 6(c) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 16 of 27
(d) Give a context-free grammar that generates precisely the language given above.
QUESTION 6(d) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 17 of 27
QUESTION 7 [12 marks] Turing Machines
(a) The following diagram shows a Turing machine, whose purpose is either to accept or
reject the input string. The input string is a string of 0’s and 1’s and the tape is blank to
the left and to the right of the input string. Initially the head is somewhere on the input
string.
(d) (Turing Machines I) The following Turing machine expects to find, as its input, a single
binary number. There are no embedded blanks and nothing else on the tape.
(i) For each of the inputs 010101, 101100010 and 1111000, what will be the on the
tape when the Turing machine halts.
QUESTION 5(d)(i) [3 marks]
(ii) What does this machine do, in general?
QUESTION 5(d)(ii) [3 marks]
COMP2600 (Formal Methods in Software Engineering) Page 24 of 32
(i) For each of the strings 010101, 101100010 and 1111000 determine the content of
the tape after the machine has terminated with the given string as an input.
QUESTION 7(a)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 18 of 27
(ii) Given an input string s, describe the output after the machine has terminated on input
string s.
QUESTION 7(a)(ii) [3 marks]
(iii) Explain (no formal proof required) why the machine will always terminate, regardless
of the given input string.
QUESTION 7(a)(iii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 19 of 27
(b) Design a Turing Machine that will take a pair of binary numbers, separated by a hash symbol
(#), and reverses their order. That is, 0101#1111 should be replaced by 1111#0101
on the tape. Assume that the tape is empty apart from the input and that the tape head
is somewhere over the input initially. Include a brief description of the purpose of the
individual states.
QUESTION 7(b) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 20 of 27
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 21 of 27
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 22 of 27
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the
corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 23 of 27
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the
corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 24 of 27
Appendix 1 — Natural Deduction Rules
Propositional Calculus
q (a is not free in q)
COMP1600/COMP6260 (Foundations of Computation) Page 25 of 27
Appendix 2 — Truth Table Values
p q p ∨ q p ∧ q p → q ¬ p p ⇔ q
T T T T T F T
T F T F F F F
F T T F T T F
F F F F T T T
COMP1600/COMP6260 (Foundations of Computation) Page 26 of 27
Appendix 3 — Hoare Logic Rules
• Precondition Strengthening:
Ps → Pw {Pw} S {Q}
{Ps} S {Q}
• Postcondition Weakening:
{P} S {Qs} Qs → Qw
{P} S {Qw}
• Assignment:
{Q(e)} x := e {Q(x)}
• Sequence:
{P} S1 {Q} {Q} S2 {R}
{P} S1; S2 {R}
• Conditional:
{P ∧ b} S1 {Q} {P ∧ ¬ b} S2 {Q}
{P} if b then S1 else S2 {Q}
• While Loop:
{P ∧ b} S {P}
{P} while b do S {P ∧ ¬ b}
(Foundations of Computation)
Writing Period: 3 hours duration
Study Period: 15 minutes duration
Permitted Materials: One A4 page with hand-written notes on both sides
Answer ALL questions
Total marks: 100
The questions are followed by labelled blank spaces into which your answers are to be written.
Additional answer panels are provided (at the end of the paper) should you wish to use more
space for an answer than is provided in the associated labelled panels. If you use an additional
panel, be sure to indicate clearly the question and part to which it is linked.
The following spaces are for use by the examiners.
Q1 (Logic) Q2 (ND) Q3 (SI) Q4 (HL) Q5 (FSA) Q6 (CFL)
Q7 (TM) Total
COMP1600/COMP6260 (Foundations of Computation) Page 1 of 27
QUESTION 1 [14 marks] Logic
Recall that two formulae are equivalent if they have have the same truth values for all variable
assignments, and consider the following set of formulae:
• (p ∧ q) ∨ (¬p ∧ ¬q)
• ¬p ∨ q
• (p ∨ ¬q) ∧ (q ∨ ¬p)
• ¬(p ∨ q)
• (q ∧ p) ∨ ¬p
(a) Identify two formulae in the above set of formulae that are equivalent, and demonstrate
their equivalence by means of a truth table.
QUESTION 1(a) [4 marks]
(b) Identify two formulae in the above set of formulae that are not equivalent, and demonstrate
the fact that they are not equivalent by a variable assignment.
QUESTION 1(b) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 2 of 27
(c) State whether the following formulae are true or false where x, y and z range over the
integers, and justify your answer briefly.
(1). ∀ x ∃ y(2x − y) = 0
(2). ∃ x ∀ y(2x − y) = 0
(3). ∀ x ∃ y(x − 2y) = 0
QUESTION 1(c) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 3 of 27
QUESTION 2 [16 marks] Natural Deduction
The following questions ask for proofs using natural deduction. Present your proofs in the Fitch
style as used in lectures. You may only use the introduction and elimination rules given in
Appendix 1. Number each line and include justifications for each step in your proofs.
(a) Give a natural deduction proof of the formula p ∨ (p → q). In this proof, you may use the
law of excluded middle (LEM) p ∨ ¬p in addition to the rules provided in the appendix.
That is, you may state p ∨ ¬p at any line in the proof, where p can stand for an arbitrary
formula, and justify this by (LEM).
QUESTION 2(a) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 4 of 27
(b) Give a natural deduction proof of the rule
∃ xP(x) ∧ ∀ x ∀ y(R(x, y) → P(y))
∃ x ∀ y(R(x, y) → P(y))
using only the rules in the appendix.
QUESTION 2(b) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 5 of 27
QUESTION 3 [16 marks] Structural Induction
(a) Consider the function subl that computes the list of sub-lists of a given list:
subl :: [a] -> [[a]]
subl [] = [[]] -- S1
subl (x:xs) = (subl xs) ++ map (pref x) (subl xs) -- S2
where the functions map, pref and ++ are given by:
map :: (a -> b) -> [a] -> [b]
map f [] = [] -- M1
map f (x:xs) = (f x):(map f xs) -- M2
pref :: a -> [a] -> [a]
pref x l = x:l -- P
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- A1
(x:xs) ++ ys = x : (xs ++ ys) -- A2
Show, using structural induction, that
length (subs l) = 2length l
for all lists l of type a.
Here, we assume the standard definition of the length function
length [] = 0 -- L1
length (x:xs) = 1 + length xs -- L2
and you may use the fact that map preserves length, and the fact that length is compatible
with concatenation, that is the equations
length (map f xs) = length xs -- LM
length (xs ++ ys) = length xs + length ys -- LA
in your proof, with justification as indicated.
In all proofs indicate the justification (eg, the line of a definition used) for each step.
COMP1600/COMP6260 (Foundations of Computation) Page 6 of 27
(i) State and prove the base case.
QUESTION 3(a)(i) [2 marks]
(ii) State the inductive hypothesis.
QUESTION 3(a)(ii) [1 mark]
(iii) State and prove the step case goal.
QUESTION 3(a)(iii) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 7 of 27
(b) Give an inductive proof the fact that left folding is compatible with list concatenation.
Consider the following definition of left folding:
foldl :: :: (b -> a -> b) -> b -> [a] -> b
foldl f z [] = z -- F1
foldl f z (x:xs) = foldl f (f z x) xs -- F2
and consider a fixed function f (of type b -> a -> b) and a fixed list ys (of elements of
type b) and show that
P(xs) ≡ ∀ z (foldl f z (xs ++ ys) = foldl f (foldl f z xs) ys)
holds for all lists xs (of elements of type a).
(i) State and prove the base case goal
QUESTION 3(b)(i) [2 marks]
(ii) State the inductive hypothesis
QUESTION 3(b)(ii) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 8 of 27
(iii) State and prove the step case goal.
QUESTION 3(b)(iii) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 9 of 27
QUESTION 4 [16 marks] Hoare Logic
(a) Specify a precondition P and a postcondition Q such that the Hoare-Triple {P} S {Q}
holds precisely for all programs S that never terminate.
QUESTION 4(a) [2 marks]
(b) The following piece of code is called Rem
r := x;
q := 0;
while (r >= n)
r := r - n;
q := q + 1
and computes two numbers, q and r, where
• q is the integer quotient of x by n
• r is the remainder of the division of x by n.
We wish to use Hoare Logic (Appendix 3) to show that:
{True} Rem {x = n ∗ q + r}
In the questions below (and your answers), we may refer to the loop code as Loop, the
body of the loop (i.e. r:-r-n;q:=q+1) as Body, and the initialisation assignments (i.e.
r:=x;q:=0) as Init.
(i) Given the desired postcondition {x = n ∗ q + r}, what is a suitable invariant I for
Loop?
QUESTION 4(b)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 10 of 27
(ii) Prove that your answer to the previous question is indeed a loop invariant. That is,
if we call your invariant I, show that {I} Body {I}. Be sure to properly justify each
step of your proof.
QUESTION 4(b)(ii) [3 marks]
(iii) Using the previous result and some more proof steps show that
{True} Rem {x = n ∗ q + r}
Be sure to properly justify each step of your proof.
QUESTION 4(b)(iii) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 11 of 27
(iv) Explain why the corresponding Hoare-triple for total correctness, that is
[True]Rem[x = n ∗ q + r]
is not valid by giving a counter-example that shows that the triple above does not
hold in general.
QUESTION 4(b)(iv) [2 marks]
(v) Identify a precondition P such that the Hoare triple
[P]Rem[x = n ∗ q + r]
is valid. Explain why the Hoare-triple now holds (no formal proof in Hoare Logic
required).
QUESTION 4(b)(v) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 12 of 27
QUESTION 5 [13 marks] Finite State Automata
(a) Design a Finite State Automaton that recognises the language of all strings over the alphabet
Σ = {a, b, c} where both the string ’abc’ and the string ’cba’ occurs as a substring.
Here, a string s is a substring of a string w if w can be written as w1sw2.
QUESTION 5(a) [3 marks]
(b) Is your Finite State Automaton (above) deterministic or non-deterministic? Explain.
QUESTION 5(b) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 13 of 27
(c) What language is recognised by the following Finite State Automaton?
Describe the language in English, and give a regular expression defining the language.
QUESTION 5(c) [3 marks]
(d) Consider the statement
∀ w ∈ Σ
∗
. N
∗
(q2,w) = q2
Express this property in English. Why might it be relevant?
QUESTION 5(d) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 14 of 27
(e) For the Finite State Automaton above, prove that
∀ n ∈ N . N
∗
(q1,(aa)
n
) = q1
and hence, or otherwise, conlude that
∀ n ∈ N . N
∗
(q0,(aa)
n+1) = q1
QUESTION 5(e) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 15 of 27
QUESTION 6 [13 marks] Context-Free Grammars
(a) Design a push-down automaton that recongnises precisely the language
{a
m
b
n
| n > m > 0}
QUESTION 6(a) [4 marks]
(b) Is your automaton deterministic, or non-deterministic? Briefly justify your answer.
QUESTION 6(b) [1 mark]
(c) Demonstrate, using the pigeon hole principle or otherwise, that the language given above
is not regular.
QUESTION 6(c) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 16 of 27
(d) Give a context-free grammar that generates precisely the language given above.
QUESTION 6(d) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 17 of 27
QUESTION 7 [12 marks] Turing Machines
(a) The following diagram shows a Turing machine, whose purpose is either to accept or
reject the input string. The input string is a string of 0’s and 1’s and the tape is blank to
the left and to the right of the input string. Initially the head is somewhere on the input
string.
(d) (Turing Machines I) The following Turing machine expects to find, as its input, a single
binary number. There are no embedded blanks and nothing else on the tape.
(i) For each of the inputs 010101, 101100010 and 1111000, what will be the on the
tape when the Turing machine halts.
QUESTION 5(d)(i) [3 marks]
(ii) What does this machine do, in general?
QUESTION 5(d)(ii) [3 marks]
COMP2600 (Formal Methods in Software Engineering) Page 24 of 32
(i) For each of the strings 010101, 101100010 and 1111000 determine the content of
the tape after the machine has terminated with the given string as an input.
QUESTION 7(a)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 18 of 27
(ii) Given an input string s, describe the output after the machine has terminated on input
string s.
QUESTION 7(a)(ii) [3 marks]
(iii) Explain (no formal proof required) why the machine will always terminate, regardless
of the given input string.
QUESTION 7(a)(iii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 19 of 27
(b) Design a Turing Machine that will take a pair of binary numbers, separated by a hash symbol
(#), and reverses their order. That is, 0101#1111 should be replaced by 1111#0101
on the tape. Assume that the tape is empty apart from the input and that the tape head
is somewhere over the input initially. Include a brief description of the purpose of the
individual states.
QUESTION 7(b) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 20 of 27
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 21 of 27
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 22 of 27
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the
corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 23 of 27
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the
corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 24 of 27
Appendix 1 — Natural Deduction Rules
Propositional Calculus
q (a is not free in q)
COMP1600/COMP6260 (Foundations of Computation) Page 25 of 27
Appendix 2 — Truth Table Values
p q p ∨ q p ∧ q p → q ¬ p p ⇔ q
T T T T T F T
T F T F F F F
F T T F T T F
F F F F T T T
COMP1600/COMP6260 (Foundations of Computation) Page 26 of 27
Appendix 3 — Hoare Logic Rules
• Precondition Strengthening:
Ps → Pw {Pw} S {Q}
{Ps} S {Q}
• Postcondition Weakening:
{P} S {Qs} Qs → Qw
{P} S {Qw}
• Assignment:
{Q(e)} x := e {Q(x)}
• Sequence:
{P} S1 {Q} {Q} S2 {R}
{P} S1; S2 {R}
• Conditional:
{P ∧ b} S1 {Q} {P ∧ ¬ b} S2 {Q}
{P} if b then S1 else S2 {Q}
• While Loop:
{P ∧ b} S {P}
{P} while b do S {P ∧ ¬ b}