mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
83 lines
3.1 KiB
Plaintext
83 lines
3.1 KiB
Plaintext
theory SimpleDBPath
|
|
|
|
use int.Int
|
|
use bool.Bool
|
|
use map.Map
|
|
|
|
type book
|
|
type shelf
|
|
|
|
predicate book1 book
|
|
function shelfId1 book : int
|
|
function code1 book : int
|
|
predicate bPK1 = forall a,b : book. ((book1 a) /\ (book1 b) /\ ((code1 a) = (code1 b))) -> a = b
|
|
|
|
predicate shelf1 shelf
|
|
function numberOfBooks1 shelf : int
|
|
function id1 shelf : int
|
|
predicate sCK1 = forall a : shelf. (numberOfBooks1 a) > 0
|
|
predicate sPK1 = forall a,b : shelf. ((shelf1 a) /\ (shelf1 b) /\ ((id1 a) = (id1 b))) -> a = b
|
|
|
|
predicate fk1 = forall a : book. (book1 a) -> (exists b : shelf. (shelf1 b) /\ ((shelfId1 a) = (id1 b)))
|
|
|
|
type javaList = { isNull : bool ; size : int ; elements : (map int int) }
|
|
|
|
constant newbooks1 : javaList
|
|
predicate r0 = (newbooks1.isNull = False) -> (newbooks1.size >= 0)
|
|
|
|
constant i1 : int
|
|
predicate r1 = (i1 = 0)
|
|
|
|
constant addedbooks1 : javaList
|
|
predicate r2 = (addedbooks1.isNull = False) /\ (addedbooks1.size = 0)
|
|
|
|
predicate r3 = (newbooks1.isNull = False) /\ (i1 < newbooks1.size)
|
|
|
|
constant error1 : int
|
|
predicate r4 = (error1 = 0)
|
|
|
|
constant theshelf1 : int
|
|
|
|
constant shelves1Size : int
|
|
function shelves1List int : shelf
|
|
function shelves1InvertedList shelf : int
|
|
function shelves1Trigger int : bool
|
|
predicate r5 = (shelves1Size >= 0) /\ ((shelves1Size = 0) -> forall c : shelf. not ((shelf1 c) /\ ((id1 c) = theshelf1)))
|
|
predicate r6 = forall c : shelf. ((shelf1 c) /\ ((id1 c) = theshelf1)) ->
|
|
(((shelves1InvertedList c) >= 0) /\ ((shelves1InvertedList c) < shelves1Size))
|
|
predicate r7 = forall c : shelf. ((shelf1 c) /\ ((id1 c) = theshelf1)) -> (c = (shelves1List (shelves1InvertedList c)))
|
|
predicate r8 = forall i : int. ((i >= 0) /\ (i < shelves1Size)) ->
|
|
(i = (shelves1InvertedList (shelves1List i)))
|
|
predicate r9 = forall i : int. ((i >= 0) /\ (i < shelves1Size)) ->
|
|
((shelf1 (shelves1List i)) /\ ((id1 (shelves1List i)) = theshelf1) )
|
|
predicate r10 = (0 >= shelves1Size) -> (shelves1Trigger 1)
|
|
predicate r11 = forall i : int.
|
|
((i >= 0) /\ (i < shelves1Size)) -> (shelves1Trigger (i + 1))
|
|
|
|
predicate r12 = (shelves1Size >= 1)
|
|
|
|
function numberOfBooks2 shelf : int
|
|
predicate r13 = forall p : shelf. (((shelf1 p) /\ (not ((id1 p) = theshelf1))) \/ (not (shelf1 p))) -> ((numberOfBooks2 p) = (numberOfBooks1 p))
|
|
predicate r14 = forall p : shelf. ((shelf1 p) /\ ((id1 p) = theshelf1)) -> ((numberOfBooks2 p) = ((numberOfBooks1 p) + 1))
|
|
predicate r15 = forall a : shelf. (numberOfBooks2 a) > 0
|
|
|
|
|
|
predicate r16 = (exists a : book. (book1 a) /\ ((code1 a) = (Map.get (newbooks1.elements) i1))) \/ (forall a : shelf. (shelf1 a) -> (not ((id1 a) = theshelf1)))
|
|
predicate r17 = (not (newbooks1.isNull))
|
|
predicate r18 = (i1 >= 0)
|
|
predicate r19 = (i1 < (newbooks1.size))
|
|
|
|
constant error2 : int
|
|
predicate r20 = (error2 = 1)
|
|
|
|
predicate r21 = (not (error2 = 0))
|
|
|
|
constant i2 : int
|
|
predicate r22 = (i2 = i1 + 1)
|
|
|
|
predicate r23 = (not ((not (newbooks1.isNull)) /\ (i2 < (newbooks1.size))))
|
|
|
|
goal G: not (bPK1 /\ sCK1 /\ sPK1 /\ fk1 /\ r0 /\ r1 /\ r2 /\ r3 /\ r4 /\ r5 /\ r6 /\ r7 /\ r8 /\ r9 /\ r10 /\ r11 /\ r12 /\ r13 /\ r14 /\ r15 /\ r16 /\ r17 /\ r18 /\ r19 /\ r20 /\ r21 /\ r22 /\ r23)
|
|
|
|
end
|