UP to CSCI 550 root document?
Note: I changed the due date on this homework from Thursday, 5 September, to Tuesday, 10 September.
Prove the following theorems from A Programmer's Introduction to Predicate Logic. In a proof of a theorem you may use any axiom or theorem appearing above the theorem (i.e., smaller number) in the list and any of the applicable proof techniques we discussed in class.
You may want to do several other theorems for your own study.
UP to CSCI 550 root document?
Do the following exercises.
UP to CSCI 550 root document?
X[0..N)
is given,
where N >= 1
.
X
is increasing.
X
are distinct.
X
are equal.
X
contains a 1
,
then X
contains a 0
as well.
X
are equal.
X
occurs only once in X
.
r
is the length of a longest constant section of
X
.
X
are prime numbers.
X
equals the
number of even-valued elements.
r
is the product of the positive elements of
X
.
r
is the maximum of the sums of the sections of
X
.
X
contains a square.
UP to CSCI 550 root document?
The notation in this online version of the assignment differs from the
printed handout. Below OR
, AND
, and
EQUIV
represent logical disjunction, conjunction, and
equivalence, respectively; **
denotes exponentiation;
!=
, <=
, and >=
denote
not-equal, less-or-equal, and greater-or-equal, respectively;
[]
denotes the guard separator box.
div
denote integer division and mod
denote the modulo operation. For any integers a
,
b
, q
, and r
such that
b != 0
:
a div b = q OR a mod b = r EQUIV a = q * b + r OR 0 <= r < |b|.Determine the weakest predicate
Q
for each of the following
expressions:
|[ var x : int { Q } ;
x := x + 1 { x > 0 } ]|
|[ var x : int { Q } ;
x := x * x { x > 0 } ]|
|[ var x : int { Q } ;
x := x * x * x - 2 * x + 4 { x > 0 } ]|
|[ var x : int { Q } ;
x := x + 1 { x**3 - 5 * x**2 + 2 * x > 0 } ]|
|[ var x : int { Q } ;
x := x * x * x - 2 * x + 4 { x**3 - 5 * x**2 + 2 * x > 0 } ]|
|[ var x : int { Q } ;
x := x + 1 { x = x + 1 } ]|
|[ var x : int { Q } ;
x := E { x = E } ]|
|[ var x : int { Q } ;
x := x mod 2 { x = x mod 2 } ]|
|[ var x,y : int { Q } ;
x,y := x+1, y-1 { x + y > 0 } ]|
|[ var x,y : int { Q } ;
x,y := y+1, x-1 { x > 0 } ]|
|[ var x,y : int { Q } ;
x,y := y * x, x*y { x + y > 0 } ]|
|[ var x, y : bool { Q } ;
x := x EQUIV y { x } ]|
|[ var x : int { Q } ;
x := x * x; x := x+1 { x > 0 } ]|
|[ var x, y : int { Q } ;
x := y ; y := x { x = A AND y = B } ]|
|[ var i : int ; var b[0..12) : array of int
{ 0 <= i < 12 OR Q } ; b.i, b.(i+1) := 3, 4 { b.i = 3 } ]|
|[ var x, y : int { true } ; if x >= y --> skip [] y >= x --> x,y := y,x fi { x >= y } ]|
UP to CSCI 550 root document?
|[ con N : int { N >= 0 } ; var f[0..N) : array of int ; var b : bool ; var n : int ; b, n := false, 0 ; do n != N --> b := b OR (f.n = 0) ; n := n + 1 od { b = (EXISTS i : 0 <= i < N : f.i = 0) } ]|
|[ con N : int { N >= 0 } ; var f[0..N) : array of int ; var b : bool ; var n : int ; b, n := false, 0 ; do n != N & NOT b --> b := b OR (f.n = 0) ; n := n + 1 od { b = (EXISTS i : 0 <= i < N : f.i = 0) } ]|
|[ var x, y, z : int { true } ; do x < y --> x, y := y, x [] y < z --> y, z := z, y od { x >= y & y >= z } ]|
UP to CSCI 550 root document?
Note that I have postponed the due date from that printed on the handout sheet.
|[ con N : int { N >= 1 }; f[0..N): array of int; var x, y : int; x, y := 0, N - 1; do x != y --> if f.x <= f.y --> x := x + 1 [] f.y <= f.x --> y := y - 1 fi od { f.x = (MAX i : 0 <= i < N : f.i) } |]Hint: What is always found in the subarray
f[x..y]
?
UP to CSCI 550 root document?
S
that does not contain
the multiplication operator. Show the derivation and a proof of the
correctness of your solution.
|[ con X, Y : int { X >= 0 & Y >= 0 } ; var z : int ; S { z : z = X * Y } ]|
S
that does not contain an
exponentiation. Show the derivation and the proof obligations.
|[ con N : int { N >= 0 } ; var b[0..N) : array of int ; S { z : z = (SUM i : 0 <= i < N : (-1)**i * b.i ) } ]|
UP to CSCI 550 root document?
S
satisfying the following
specification. Show the derivation and the proof obligations.
|[ con N : int { N >= 1 } ; var b[0..N) : array of int ; var r : int ; S { r : r = (# i,j : 0 <= i < j < N : b.i*b.j >= 0 ) } ]|Hint: Consider the cases for
x
andy y
in
which x*y >= 0
.
UP to CSCI 550 root document?