Algorithms and Data Structures (INF1, Autumn'05)
Exercise Set 6
Exercise 1:
Assume that you are given a function sum(l:LIST):int which
for an input list l=< a1,a2, ..., an>
returns the sum of all its values, i.e.,
sum(l)=a1.value + a2.value + ... + an.value.
Formally, we know that the function sum is totally correct w.r.t. the following
pre- and post-conditions.
--pre: l=< a1,a2, ..., an> s.t.
VALUE_TYPE=int
x:=sum(l)
--post: x=Σi = 1..n ai.value
- Using only this information about sum, can you now prove the following?
--pre: l=< a1,a2, ..., an> s.t.
VALUE_TYPE=int
x:=sum(l)
y:=sum(l)
--post: x+y=2.Σi = 1..n ai.value
- If yes, then prove it.
- If no, say why not. Modify the pre- or post-condition
of the function sum defined in the beginning such that the
statement above is true, and prove it.
Exercise 2:
-
Define a function find(i:int, l:LIST):ENTRY_TYPE such
that it is totally correct with regard to the following pre- and
post- conditions.
--pre: l=< a1,a2, ..., an> and i>0
x:=find(i,l)
--post: x = ai if 1 <= i <= n and x = NIL otherwise; and l'=l
- When using the doubly-linked list
implementation of LIST we know that all the
basic operations in the worst-case take time O(1). What is the
worst-case time complexity
of your function find, taking |l| (the number of entries in the list l)
as the size of the input?
Exercise 3 (hand-in):
Write appropriate pre- and post-conditions for the list operations
first and next.
--pre: ???
x:=l.first
--post: ???
--pre: ???
y:=l.next(x)
--post: ???