Subject: Principles of formal software development
1) The following Java class with JML annotations implements a counter that starts at value 0 and each time it is incremented, its value increases by 1. The counter can never increase beyond a certain maximum value capacity. The constructor for this class (the method called Counter) creates and initializes a new counter with initial value of 0, and capacity set to the input parameter max val.
public class Counter {
private /*@ spec_public @*/ int val;
private /*@ spec_public @*/ int capacity;
/*@ public invariant 0 <= val && val <= capacity; @*/
/*@ requires val < capacity;
@ modifiable val;
@ ensures val == old(val+1); @*/
public void increment()
/*@ ensures result == val; @*/
public /*@ pure @*/ int get_val()
public boolean find(int[] a, int x)
public Counter(int max_val)
{
capacity = max_val;
val = 0;
}
}
(a) Write the JML specification of the constructor (the Counter method). Note that the capacity should always be positive. The postcondition must express that the values of the instance variables (initial value of counter and its capacity) are set correctly.
(b) Write the a JML specification of the find method. This method must return true if the value x occurs in any of the of the first val positions in the array a, where val is the current value of the counter, and returns false otherwise. The specifications must guarantee that there will never be an array out of bounds error. In other words, the input array must be of adequate size, which means that it must have at least val positions. Also, we restrict the method to work only on arrays up to a maximum size of capacity.
c) Write code for the find method that meets your specification for part (b) above. If you are not familiar with Java, you may use another programming language syntax, such as the programming language augmented with arrays and Booleans.
2) Below is a modified version of the program in the course notes which computes the sum of the values in an integer list. The machine instructions are the same. Only some INV statements and the postcondition are different.
Precondition: (r0 :m intlist ∧ r3 = 0)
Π1 : ADD r1 := r3 + r3
Π2 : INV (r0 :m intlist ∧ r1 :m int ∧ r3 = 0)
Π3 : LD r5 := m(r0 + 0)
Π4 : INV (r0 :m intlist ∧ r1 :m int ∧ r3 = 0 ∧ r5 = m(r0))
Π5 : BEQ (r5 = r3) 7
Π6 : LD r2 := m(r0 + 1)
Π7 : LD r0 := m(r0 + 2)
Π8 : ADD r1 := r1 + r2
Π9 : INV (r0 :m intlist ∧ r1 :m int ∧ r3 = 0)
Π10 : BEQ (r3 = r3) − 7
Π11 : INV (r1 :m int)
Π12 : ADDC r0 := r1 + 0
Π13 : RET
Postcondition: (r0 :m int)
(a) Using this modified definition, find the verification condition of this new version of the program using the method described in class (the VCG method). Show each V Ci for i = 1, . . . , 13.
(b) Explain informally (a few sentences) why this verification condition is provable.
(c) Prove the verification condition form question (2). In addition to the rules of propositional logic, and the usual laws of integer arithmetic, the rules listed on the next page can be used. Note that these rules include named versions of the typing and safety rules in the course notes. Your verification condition should have 5 conjuncts.
0 comments