tests/SimpleDBPathSansListes.why

   1 theory SimpleDBPath
   2
   3 use int.Int
   4
   5 type book
   6 type shelf
   7
   8 predicate book1 book
   9 function shelfId1 book : int
  10 function code1 book : int
  11 predicate bPK1 = forall a,b : book. ((book1 a) /\ (book1 b) /\ ((code1 a) = (code1 b))) -> a = b
  12
  13 predicate shelf1 shelf
  14 function numberOfBooks1 shelf : int
  15 function id1 shelf : int
  16 predicate sCK1 = forall a : shelf. (numberOfBooks1 a) > 0
  17 predicate sPK1 = forall a,b : shelf. ((shelf1 a) /\ (shelf1 b) /\ ((id1 a) = (id1 b))) -> a = b
  18
  19 predicate fk1 = forall a : book. (book1 a) -> (exists b : shelf. (shelf1 b) /\ ((shelfId1 a) = (id1 b)))
  20
  21 constant i1 : int
  22 predicate r1 = (i1 = 0)
  23
  24 constant error1 : int
  25 predicate r4 = (error1 = 0)
  26
  27 constant theshelf1 : int
  28
  29 constant shelves1Size : int
  30 function shelves1List int : shelf
  31 function shelves1InvertedList shelf : int
  32 predicate shelves1Trigger int
  33 predicate r5 = (shelves1Size >= 0) /\ ((shelves1Size = 0) -> forall c : shelf. not ((shelf1 c) /\ ((id1 c) = theshelf1)))
  34 predicate r6 = forall c : shelf. ((shelf1 c) /\ ((id1 c) = theshelf1)) ->
  35         (((shelves1InvertedList c) >= 0) /\ ((shelves1InvertedList c) < shelves1Size))
  36 predicate r7 = forall c : shelf. ((shelf1 c) /\ ((id1 c) = theshelf1)) -> (c = (shelves1List (shelves1InvertedList c)))
  37 predicate r8 = forall i : int. ((i >= 0) /\ (i < shelves1Size)) ->
  38         (i = (shelves1InvertedList (shelves1List i)))
  39 predicate r9 = forall i : int.  ((i >= 0) /\ (i < shelves1Size)) ->
  40            ((shelf1 (shelves1List i)) /\ ((id1 (shelves1List i)) =  theshelf1) )
  41 predicate r10 = (0 >= shelves1Size) -> (shelves1Trigger 1)
  42 predicate r11 = forall i : int.
  43    ((i >= 0) /\ (i < shelves1Size)) -> (shelves1Trigger (i + 1))
  44
  45 predicate r12 = (shelves1Size >= 1)
  46
  47 function numberOfBooks2 shelf : int
  48 predicate r13 = forall p : shelf. (((shelf1 p) /\ (not ((id1 p) = theshelf1))) \/ (not (shelf1 p))) -> ((numberOfBooks2 p) = (numberOfBooks1 p))
  49 predicate r14 = forall p : shelf.  ((shelf1 p) /\ ((id1 p) = theshelf1)) -> ((numberOfBooks2 p) = ((numberOfBooks1 p) + 1))
  50 predicate r15 = forall a : shelf.  (numberOfBooks2 a) > 0
  51
  52 constant newbooks1 : int
  53
  54
  55 predicate r16 = (exists a : book. (book1 a) /\ ((code1 a) = newbooks1)) \/ (forall a : shelf. (shelf1 a) -> (not ((id1 a) = theshelf1)))
  56
  57 constant error2 : int
  58 predicate r20 = (error2 = 1)
  59
  60 predicate r21 = (not (error2 = 0))
  61
  62 constant i2 : int
  63 predicate r22 = (i2 = i1 + 1)
  64
  65 goal G: not (bPK1 /\ sCK1 /\ sPK1 /\ fk1 /\ r1 /\ r4 /\ r5 /\ r6 /\ r7 /\ r8 /\ r9 /\ r10 /\ r11 /\ r12 /\ r13 /\ r14 /\ r15 /\ r16 /\ r20 /\ r21 /\ r22 )
  66
  67 end