[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] arrays

 i am doing my m-tech project using pvs theorem prover.from site i got a paper related to arrays.it is as follows....
% Arrays: function version
arrays[elem: TYPE+]: THEORY
arr: TYPE = [ nat, [nat -> elem] ]
a,b: VAR arr
n, i, j: VAR nat
e: VAR elem
anyelem: elem
anyarray: arr
new (n): arr = (n, (lambda n: anyelem))
length(a): nat = a`1
put(a, i, e): arr =
IF i < a`1 THEN (a`1, a`2 WITH [(i) := e]) ELSE anyarray ENDIF
get(a, i): elem =
IF i < a`1 THEN a`2(i) ELSE anyelem ENDIF
length1: THEOREM
length(new(n)) = n
length2: THEOREM
FORALL(a, i, e):
0 <= i AND i < length(a) IMPLIES
length(put(a, i, e)) = length(a)
FORALL(a, i, e):
0 <= i AND i < length(a) IMPLIES
get(put(a, i, e), i) = e
FORALL(a, i, j, e):
0 <= i AND i < length(a) AND
0 <= j AND j < length(a) AND i /= j IMPLIES
get(put(a, i, e), j) = get(a, j)
unassigned: AXIOM
FORALL(a, i): i >= a`1 IMPLIES a`2(i) = anyelem
equality: THEOREM
FORALL(a, b):
a = b IFF
length(a) = length(b) AND
FORALL(i): 0 <= i AND i < length(a) IMPLIES get(a,i) = get(b,i)
END arrays
i want to use this in my program.ie for modellind arrays in 'c' program using PVS.
ie.i want to use an array say A[10] and i want to put elements and get elements.how can i use the above theorem for that purpose.please giv e me some hints.

From the happening headlines to the juiciest gossip, get your daily update on MSN India Drag n' drop