辅导R语言程序|辅导Python程序|辅导Haskell程序|讲解C/C++编程
- 首页 >> Algorithm 算法 Assignment 2 CSSE3100/7100 Reasoning about Programs
Due: 1pm on 10 May, 2022
The aim of this assignment is to provide you with experience in specifying and deriving
array-based algorithms, and verifying them using Dafny. It is worth 20% of your final mark
for the course.
Instructions: Submit a Dafny file for each of Q1 and Q2, and if you are a CSSE7100
student for Q3. These files should be submitted to Blackboard by the due date and time.
1. A sequence is said to be monotonically non-decreasing if it either consists of only one
element, or it consists of two or more elements where these elements are in non-descending
order. The following function mono determines whether the sequence a[i..j] is monotonically
decreasing.
function mono(a: array, i: nat, j: nat): bool
requires a.Length > 0 && 0 <= i < j <= a.Length
reads a
decreases j - i {
if j == i + 1 then true
else if a[i] <= a[i + 1] then mono(a, i + 1, j) else false
}
Your friend writes a method to return the index r of an array a such that a[0..r] is the longest
monotonically non-decreasing sequence in a starting at a[0].
method M(a:array) returns (r: int)
requires a.Length > 0
ensures 1 <= r <= a.Length && mono(a, 0, r) && (r == a.Length || a[r - 1] > a[r])
{
r := 1;
while r < a.Length && a[r - 1] <= a[r]
invariant 1 <= r <= a.Length
invariant mono(a, 0, r)
{
r := r + 1;
} }
Unfortunately, he can't get it to verify in Dafny.
Your task: Write and prove a lemma which allows Dafny to verify your friend's program
when a call to the lemma is made from his code. Note you must not change the specification,
loop invariant or code above except to add a call to your lemma. (4 marks)
2. You have been asked to write a program PatternReplace which searches an integer array a
for a pattern of elements (provided in a strictly smaller integer array p) and
a) replaces the first occurrence of the pattern in a by another pattern of the same size
(provided in an integer array q), and
b) returns the position of the start of the pattern it replaced, if any, and -1 otherwise.
For example, if a were [2, 1, 2, 3, 4, 2, 3, 5], p were [2, 3] and q were [0, 0] then the program
should change a to [2, 1, 0, 0, 4, 2, 3, 5] and return 2.
If on the other hand p were [3, 2] and a and q were as before then the program would not
change a and return -1.
Your colleague suggests the following strategy for writing the program using 2 loops, an
outer and an inner loop. The outer loop iterates over the indices of the array a starting from 0.
For each index, it uses the inner loop to check whether the pattern in p is in a starting from
that index. If so, it sets r to that index and on this and the next p.Length-1 iterations of the
outer loop replaces the elements in a by those of q. To do this replacement, you can introduce
a local variable count which is initially p.Length and which reduces by 1 on each
replacement. When it reaches 0, you're done!
You like this strategy but want to be sure your algorithm is correct, so you are going to use
Dafny to verify it. You already realise you can use wishing to introduce count.
Your task: Write a Dafny program following your colleague's strategy including the
necessary specifications and loop invariants to verify it. You are not allowed to use break or
return statements or Dafny's mathematical types, such as sequences, in your code. You may
use Dafny's mathematical types in specifications.
For each loop invariant state which loop design technique you used to derive the invariant, or
otherwise state the reason the invariant was introduced, e.g., to place bounds on a variable
used as an array index. To simplify your predicates (and hence manage complexity!) it is recommended that you
a) Use multiple ensures clauses and invariants. Keep them as simple as possible. You
will find that you need many postconditions and invariants. Don't forget that there
may be different cases for when r == -1 and when r != -1.
b) Define a Boolean function IsStart, which determines whether an index i, in array (or
equivalent sequence) a is the start of the pattern defined by array (or equivalent
sequence) p. That is, for the first example above, i == 2 or i == 5 would result in true,
whereas i == 0 or i == 1 would result in false.
c) Avoid predicates with nested quantifications where possible. Dafny sometimes has
trouble reasoning about these without lemmas. (You should not need lemmas for this
question.) Note that a predicate like a[n..m] == 0 is essentially using universal
quantification. That is, a[n..m] == 0 is equivalent to forall i :: n <= i < m ==> a[i] == 0.
You may find this question challenging and not be able to get Dafny to verify your program.
Be assured you will get part marks for every correct part of your specification and invariants,
even if your program does not verify. (16 marks)
3. (CSSE7100 students only) The program of Q2 searches for the first occurrence of the
pattern p in a and replaces it with the pattern q, returning its starting position in r.
(a) Write a method header including pre- and postcondition specifications for a program
which performs the same search and replace starting from an index j, where j is provided as
an additional input. There is no need to provide invariants or code for this program.
(b) Write a method header including pre- and postcondition specifications for a program
which replaces all patterns p in a with q, returning true in r when there has been at least one
replacement and false otherwise. There is no need to provide invariants or code for this
program.
In both parts of this question, you may use your IsStart function from Q2. It is not required
that you avoid nested quantifications in this question. (4 marks)
Marking
In each question, you will get marks for parts of your specifications, invariants, etc. which are
correct even if your entire answer is not correct, e.g., your program is not verifying.
For Q1, the distribution of marks is 2.5 marks for the lemma header including specification,
0.5 marks for the lemma call, and 1 mark for the lemma proof.
For Q2, the distribution is 4.5 marks for the method header including specification, 8 marks
for loop invariants (including comments about derivation) and termination metrics (if not
automatically provided), and 3.5 marks for your code.
For Q3, each of the method specifications is worth 2 marks.
CSSE7100 students will be given a mark out of 24 which will then be scaled to their final
mark for the assignment out of 20.
School Policy on Student Misconduct
This assignment is to be completed individually. You are required to read and understand the
School Statement on Misconduct, available on the School's website at:
http://www.itee.uq.edu.au/itee-student-misconduct-including-plagiarism
Due: 1pm on 10 May, 2022
The aim of this assignment is to provide you with experience in specifying and deriving
array-based algorithms, and verifying them using Dafny. It is worth 20% of your final mark
for the course.
Instructions: Submit a Dafny file for each of Q1 and Q2, and if you are a CSSE7100
student for Q3. These files should be submitted to Blackboard by the due date and time.
1. A sequence is said to be monotonically non-decreasing if it either consists of only one
element, or it consists of two or more elements where these elements are in non-descending
order. The following function mono determines whether the sequence a[i..j] is monotonically
decreasing.
function mono(a: array
requires a.Length > 0 && 0 <= i < j <= a.Length
reads a
decreases j - i {
if j == i + 1 then true
else if a[i] <= a[i + 1] then mono(a, i + 1, j) else false
}
Your friend writes a method to return the index r of an array a such that a[0..r] is the longest
monotonically non-decreasing sequence in a starting at a[0].
method M(a:array
requires a.Length > 0
ensures 1 <= r <= a.Length && mono(a, 0, r) && (r == a.Length || a[r - 1] > a[r])
{
r := 1;
while r < a.Length && a[r - 1] <= a[r]
invariant 1 <= r <= a.Length
invariant mono(a, 0, r)
{
r := r + 1;
} }
Unfortunately, he can't get it to verify in Dafny.
Your task: Write and prove a lemma which allows Dafny to verify your friend's program
when a call to the lemma is made from his code. Note you must not change the specification,
loop invariant or code above except to add a call to your lemma. (4 marks)
2. You have been asked to write a program PatternReplace which searches an integer array a
for a pattern of elements (provided in a strictly smaller integer array p) and
a) replaces the first occurrence of the pattern in a by another pattern of the same size
(provided in an integer array q), and
b) returns the position of the start of the pattern it replaced, if any, and -1 otherwise.
For example, if a were [2, 1, 2, 3, 4, 2, 3, 5], p were [2, 3] and q were [0, 0] then the program
should change a to [2, 1, 0, 0, 4, 2, 3, 5] and return 2.
If on the other hand p were [3, 2] and a and q were as before then the program would not
change a and return -1.
Your colleague suggests the following strategy for writing the program using 2 loops, an
outer and an inner loop. The outer loop iterates over the indices of the array a starting from 0.
For each index, it uses the inner loop to check whether the pattern in p is in a starting from
that index. If so, it sets r to that index and on this and the next p.Length-1 iterations of the
outer loop replaces the elements in a by those of q. To do this replacement, you can introduce
a local variable count which is initially p.Length and which reduces by 1 on each
replacement. When it reaches 0, you're done!
You like this strategy but want to be sure your algorithm is correct, so you are going to use
Dafny to verify it. You already realise you can use wishing to introduce count.
Your task: Write a Dafny program following your colleague's strategy including the
necessary specifications and loop invariants to verify it. You are not allowed to use break or
return statements or Dafny's mathematical types, such as sequences, in your code. You may
use Dafny's mathematical types in specifications.
For each loop invariant state which loop design technique you used to derive the invariant, or
otherwise state the reason the invariant was introduced, e.g., to place bounds on a variable
used as an array index. To simplify your predicates (and hence manage complexity!) it is recommended that you
a) Use multiple ensures clauses and invariants. Keep them as simple as possible. You
will find that you need many postconditions and invariants. Don't forget that there
may be different cases for when r == -1 and when r != -1.
b) Define a Boolean function IsStart, which determines whether an index i, in array (or
equivalent sequence) a is the start of the pattern defined by array (or equivalent
sequence) p. That is, for the first example above, i == 2 or i == 5 would result in true,
whereas i == 0 or i == 1 would result in false.
c) Avoid predicates with nested quantifications where possible. Dafny sometimes has
trouble reasoning about these without lemmas. (You should not need lemmas for this
question.) Note that a predicate like a[n..m] == 0 is essentially using universal
quantification. That is, a[n..m] == 0 is equivalent to forall i :: n <= i < m ==> a[i] == 0.
You may find this question challenging and not be able to get Dafny to verify your program.
Be assured you will get part marks for every correct part of your specification and invariants,
even if your program does not verify. (16 marks)
3. (CSSE7100 students only) The program of Q2 searches for the first occurrence of the
pattern p in a and replaces it with the pattern q, returning its starting position in r.
(a) Write a method header including pre- and postcondition specifications for a program
which performs the same search and replace starting from an index j, where j is provided as
an additional input. There is no need to provide invariants or code for this program.
(b) Write a method header including pre- and postcondition specifications for a program
which replaces all patterns p in a with q, returning true in r when there has been at least one
replacement and false otherwise. There is no need to provide invariants or code for this
program.
In both parts of this question, you may use your IsStart function from Q2. It is not required
that you avoid nested quantifications in this question. (4 marks)
Marking
In each question, you will get marks for parts of your specifications, invariants, etc. which are
correct even if your entire answer is not correct, e.g., your program is not verifying.
For Q1, the distribution of marks is 2.5 marks for the lemma header including specification,
0.5 marks for the lemma call, and 1 mark for the lemma proof.
For Q2, the distribution is 4.5 marks for the method header including specification, 8 marks
for loop invariants (including comments about derivation) and termination metrics (if not
automatically provided), and 3.5 marks for your code.
For Q3, each of the method specifications is worth 2 marks.
CSSE7100 students will be given a mark out of 24 which will then be scaled to their final
mark for the assignment out of 20.
School Policy on Student Misconduct
This assignment is to be completed individually. You are required to read and understand the
School Statement on Misconduct, available on the School's website at:
http://www.itee.uq.edu.au/itee-student-misconduct-including-plagiarism