%% PVS Version 4.1 - Allegro CL Enterprise Edition 8.0 [Linux (x86)] (Apr 20, 2007 0:08)
%% 8.0 [Linux (x86)] (Apr 20, 2007 0:08)
$$$PVSHOME/.pvs.lisp
;;; This is a list - the first element is the base URL, used to define the
;;; header element in the resulting files. The second element is the
;;; directory corresponding to the base URL - where the html files are
;;; stored locally. The rest of the elements
;;; are of the form (DIR URL HTMLDIR), where the DIR is the directory
;;; containing specification subdirectories and files, URL is the URL
;;; corresponding to this DIR, and HTMLDIR is the actual location of the
;;; URL. For example, the following sets base to "/homes/owre/public_html",
;;; and any pvs-files or subdirectories located in "/homes/owre/pvs-specs"
;;; cause corresponding html files and subdirectories to be located at
;;; "/homes/owre/public_html/pvs-specs".
(setq *pvs-url-mapping*
'("http://www.csl.sri.com/~owre/"
"/homes/owre/public_html/"
("/homes/owre/pvs-specs" "pvs-specs" "pvs-specs")
("/homes/owre/pvs3.0" "pvs-specs/pvs3.0" "pvs-specs/pvs3.0")
("/homes/owre/pvs-validation/3.0/libraries/LaRC/lib"
"pvs-specs/validation/nasa"
"pvs-specs/validation/nasa")))
;;(lf "store-object")
;; (defmethod replace-expr* (lhs rhs (expr binding-expr) lastopinfix?)
;; (if (replace-eq lhs expr)
;; (parenthesize rhs lastopinfix?)
;; (let ((*bound-variables* (append (bindings expr) *bound-variables*)))
;; (lcopy expr
;; 'expression (replace-expr* lhs rhs (expression expr) nil)))))
(setq aaa 3)
$$$PVSHOME/.pvsemacs
;;(load "~owre/emacs/cmh-pvs-prover-helps")
(pvs-send-and-wait "#+cmu (load (make-pathname :defaults (user-homedir-pathname) :name \".pvs\" :type \"lisp\")) #-cmu nil")
;;(load-prelude-library "Field")
; (if (string-match "pvs3.0/validation" *pvs-current-directory*)
; (progn (set-decision-procedure 'ics)
; (pvs-send "(setq *force-dp* t)")
; (message "Set *force-dp* to t")))
(setq pvs-default-timeout 30)
(setq message-log-max 500)
(defun ics-is-default ()
(interactive)
(set-decision-procedure 'ics)
(pvs-send "(setq *force-dp* t)"))
(set-rewrite-depth 0)
(pvs-send "(setq *save-proofs-pretty* nil)")
;; (set-ilisp-value
;; 'comint-prompt-regexp
;; "^[ ]*\\(\\[[0-9]+i?c?\\] \\|\\[step\\] \\)?\\(\\(<[-A-Za-z]* ?[0-9]*?> \\)\\3?\\|[-A-Za-z0-9]+([0-9]+): \\)\\|Rule\\? \\|PVS EVAL: \\|(Y or N)\\|(Yes or No)\\|Please enter")
(setq pvs-print-command "enscript")
(setq pvs-print-switches '("-2r"))
(setq pvs-print-title-switches nil)
;;(setq pvs-x-show-proofs t)
;;(defvar *pvspath* pvs-path)
;(nconc auto-mode-alist '(("\\.dc$" . dc-mode)))
;
;(defun dc-mode ()
; (pvs-mode))
;
;(defun load-dc ()
; (interactive)
; (load (concat pvs-path "/dc/emacs/dc")))
(pvs-send "(pushnew \"~owre/pvs-patches\" *pvs-directories* :test #'string=)")
;;(setq pvs-wish-cmd "wish4.0")
(defun pvs-title-string ()
(format "%s%s%s:%s/"
(trailing-components pvs-path 2)
(cond ((stringp (cadddr *pvs-version-information*)) "E")
((stringp (caddr *pvs-version-information*)) "T")
((stringp (cadr *pvs-version-information*)) "R")
(t "N"))
(let ((host (car (string-split ?. (getenv "HOSTNAME")))))
(if (equal host "photon")
""
(format "@%s" host)))
(trailing-components *pvs-current-directory* 2)))
;; Sent to Myla 2006-07-24
;;(pvs-send "(setq *pvs-path* nil)")
$$$top.pvs
top: THEORY
BEGIN
IMPORTING phones, bakery, light_bakery, bijections,
expression, eval, sine, stamps
END top
$$$stamps.pvs
% This is the stamps problem:
% Given an unlimited quantity of 3 and 5 cent stamps, show that any
% postage of 8 cents or more can be met. The first one is easier to prove,
% but as i ranges over nats, i+8 must be used in the expression. The
% second spec is more natural, but a little harder to prove since it
% needs a special form of induction.
stamps : THEORY
BEGIN
i, n3, n5: VAR nat
stamps: LEMMA (FORALL i: (EXISTS n3, n5: i+8 = 3*n3 + 5*n5))
END stamps
stamps2 : THEORY
BEGIN
n3, n5: VAR nat
i: VAR upfrom[8]
stamps: LEMMA (FORALL i: (EXISTS n3, n5: i = 3*n3 + 5*n5))
END stamps2
$$$stamps.prf
(|stamps|
(|stamps| "" (INDUCT "i")
(("1" (INST + "1" "1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (CASE-REPLACE "n5!1=0")
(("1" (ASSERT)
(("1" (INST + "n3!1-3" "2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
("2" (INST + "n3!1+2" "n5!1-1")
(("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
(|stamps2|
(|stamps| "" (INDUCT "i")
(("1" (QE) (("1" (PROPAX) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (CASE-REPLACE "n5!1=0")
(("1" (ASSERT)
(("1" (INST + "n3!1-3" _)
(("1" (QE) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("2" (INST + "n3!1+2" _)
(("2" (ASSERT) (("2" (QE) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
$$$print.pvs
printing[T : TYPE+]: THEORY
BEGIN
printf(a:T, typ: string, fmt: string): bool = true
% attachment prints a as type typ with Lisp format string fmt
print(a:T, typ: string): bool = printf(a, typ, "~a ")
dumpf(a:T, fmt: string): bool = true
% attachment prints Lisp repn of a with Lisp format string fmt
dump(a:T): bool = dumpf(a, "~a ")
END printing
printstrings: THEORY
BEGIN
IMPORTING printing[real]
prints(s:string): bool = true % attachmentr prints Lisp format string s
space: bool = prints(" ")
tab: bool = prints("~0,8T")
newline: bool = prints("
")
printreal(a:real): bool = dumpf(a,"~g")
END printstrings
state[T: TYPE]: THEORY
BEGIN
write(a:T): bool = true % attachment saves a in state
innerread(i:nat): T % attachment returns saved state
read: T = innerread(3) % argument is ignored
END state
sprint: theory
begin
sprint(s:string): bool = true
space: bool = sprint(" ")
terpri: bool = sprint("
")
end sprint
print[T : TYPE+]: THEORY
BEGIN
importing sprint
x: T
print(a:T, s:string): bool = true
pvsprint(a:T, s:string): bool = true
printa(a:T): bool = print(a, " ~a")
read: T
write(a:T): bool = true
printset(a:setof[T]) : bool = forall (x:T): if member(x,a) then
printa(x) and space else true endif
END print
gprint: THEORY
BEGIN
IMPORTING print
printreal(x: number): bool = print(x, "~3g")
END gprint
$$$print.prf
(|sprint|)
(|print|)
(|gprint|)
(|test|)
(|sine| (|goo| "" (PROPAX) NIL NIL))
$$$sine.pvs
test[D,R: type]: theory
begin
importing printing, printstrings
t: type = upto(10)
printfun(f:[D->R]): bool = forall (x:D): dump(f(x))
end test
sine: theory
begin
importing test
n: var nat
x: var real
fac(n): recursive nat = if n=0 then 1 else n*fac(n-1) endif
measure n
even?(n): recursive bool = if n=0 then true elsif n=1 then false else even?(n-2) endif measure n
sin_ser(n) : real = IF even?(n) THEN 0 ELSE ((-1) ^ ((n - 1) / 2)) / fac(n) ENDIF
sin(n, x): recursive real = if n=0 then 0 else sin_ser(n) * (x ^ n) +
sin(n-1,x) endif measure n
end sine
$$$sine.prf
(test (printfun_TCC1 0 (printfun_TCC1-2 "" 3386797329 3386797329 ("" (skosimp) (("" (inst 1 "f!1(x!1)") nil nil)) nil) proved nil 91631 20 t shostak) (printfun_TCC1-1 nil 3386654200 3386654279 ("" (existence-tcc) nil nil) proved ((R formal-type-decl nil test nil) (D formal-type-decl nil test nil)) 46 20 nil nil)))(sine (fac_TCC1 0 (fac_TCC1-1 nil 3386654200 3386654279 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) 36 40 nil nil)) (fac_TCC2 0 (fac_TCC2-1 nil 3386654200 3386654279 ("" (termination-tcc) nil nil) proved nil 7 10 nil nil)) (even?_TCC1 0 (even?_TCC1-1 nil 3386654200 3386654279 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) 56 40 nil nil)) (even?_TCC2 0 (even?_TCC2-1 nil 3386654200 3386654279 ("" (termination-tcc) nil nil) proved nil 10 0 nil nil)) (sin_ser_TCC1 0 (sin_ser_TCC1-2 "" 3386796612 3386796612 ("" (induct "n" :name "NAT_induction") (("" (skosimp) (("" (expand "even?" 1) (("" (ground) (("" (inst -1 "j!1 - 2") (("" (assert) (("" (lemma "int_plus_int_is_int") (("" (inst -1 "(j!1 - 3) / 2" "1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved nil 1596764 6160 t shostak) (sin_ser_TCC1-1 nil 3386654200 3386654279 ("" (subtype-tcc) nil nil) proved ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (int_plus_int_is_int judgement-tcc nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (NAT_induction formula-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (even? def-decl "bool" sine nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)) 96 90 nil nil)) (sin_ser_TCC2 0 (sin_ser_TCC2-2 "" 3386797107 3386797107 ("" (induct "n" :name "NAT_induction") (("" (skosimp) (("" (expand "fac" -2) (("" (lift-if) (("" (ground) (("" (expand "fac" -1) (("" (lift-if) (("" (ground) (("" (inst -2 "j!1 - 2") (("" (assert) (("" (prop) (("1" (assert) (("1" (lemma "zero_times3") (("1" (inst-cp -1 "fac(j!1 - 2)" "j!1 * (j!1 - 1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "even?" 3) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved nil 460961 630 t shostak) (sin_ser_TCC2-1 nil 3386654200 3386654279 ("" (subtype-tcc) nil nil) proved ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (zero_times3 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NAT_induction formula-decl nil naturalnumbers nil) (fac def-decl "nat" sine nil) (/= const-decl "boolean" notequal nil) (even? def-decl "bool" sine nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 66 40 nil nil)) (sin_TCC1 0 (sin_TCC1-1 nil 3386654200 3386654279 ("" (subtype-tcc) nil nil) proved ((/= const-decl "boolean" notequal nil)) 12 20 nil nil)) (goo 0 (goo-1 nil 3386794914 3386794914 ("" (propax) nil nil) proved nil 16 0 t shostak)))
$$$sum.pvs
sum: THEORY
BEGIN
sum_nats(n: nat): RECURSIVE nat =
IF n=0 THEN 0 ELSE n+sum_nats(n-1) ENDIF
MEASURE n
test: LEMMA sum_nats(3) = 6
closed_form: THEOREM FORALL (n:nat): sum_nats(n) = n*(n+1)/2
bigtest: LEMMA sum_nats(100) = 5050
biggertest: LEMMA sum_nats(200) = 20100
hugetest: LEMMA sum_nats(100000) = 5000050000
END sum
summations: THEORY
BEGIN
n: VAR nat
f, g: VAR [nat -> real]
summation(f, n): RECURSIVE real =
IF n = 0
THEN f(0)
ELSE f(n) + summation(f, n - 1)
ENDIF
MEASURE n
IMPORTING sum
summation_nats: LEMMA summation(id[nat], n) = sum_nats(n)
summation_nats_closed_form: LEMMA summation(id[nat], n) = n*(n+1)/2
r: VAR real
square(r: real): real = r*r
summation_squares: LEMMA
summation(square, n) = n * (n + 1) * (2*n + 1) / 6
cube(r): real = r*r*r
summation_cubes: LEMMA
summation(cube, n) = n*n*(n+1)*(n+1)/4
summation_of_cubes_alt: LEMMA
summation(cube, n) = square(summation(id[nat],n))
summation_of_cubes_alt2: LEMMA
summation(cube, n) = square(summation(id[nat],n))
summation_of_sum: LEMMA
summation((lambda n: f(n) + g(n)), n) = summation(f, n) + summation(g, n)
% summation_times: lemma forall (c: real):
% summation((lambda n: c*f(n)), n) = c * summation(f,n)
%summation_split: lemma forall (i:nat): 0 <= i and i<=n implies
% summation(lambda n: if n<=i then 0 else f(n) endif,n) +
% summation(lambda n: if n<=i then f(n) else 0 endif,n) =
% summation(f,n)
subtype_test: LEMMA summation(square, summation(id[nat],3)) = 91
summation_of_nat_is_nat: JUDGEMENT summation(g:[nat->nat], n) HAS_TYPE nat
judgement_test: LEMMA summation(square, summation(id[nat], 3)) = 91
END summations
$$$sum.prf
(|sum| (|sum_nats_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|sum_nats_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|test| "" (GRIND) NIL NIL)
(|closed_form| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL)
(|bigtest| "" (GRIND) NIL NIL) (|biggertest| "" (GRIND) NIL NIL)
(|hugetest| "" (POSTPONE) NIL NIL))
(|summations| (|summation_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|summation_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|summation_nats| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL)
(|summation_nats_closed_form| "" (SKOSIMP)
(("" (USE* "summation_nats" "closed_form") (("" (ASSERT) NIL NIL))
NIL))
NIL)
(|summation_squares| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL)
(|summation_cubes| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL)
(|summation_of_cubes_alt| "" (SKOSIMP)
(("" (REWRITE "summation_nats_closed_form")
(("" (EXPAND "square")
(("" (GENERALIZE "n!1" "n")
(("" (INDUCT-AND-SIMPLIFY "n") NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|summation_of_cubes_alt2| ""
(GRIND :DEFS EXPLICIT :THEORIES ("sum" "summations") :EXCLUDE
("summation_of_cubes_alt"))
NIL NIL)
(|summation_of_sum| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL)
(|subtype_test_TCC1| "" (SUBTYPE-TCC))
(|subtype_test| "" (GRIND) NIL NIL)
(|summation_of_nat_is_nat| "" (INDUCT-AND-SIMPLIFY "n")
(("1" (LEMMA "int_plus_int_is_int") (("1" (INST?) NIL NIL)) NIL)
("2" (LEMMA "rat_plus_rat_is_rat") (("2" (INST?) NIL NIL)) NIL))
NIL)
(|judgement_test| "" (GRIND) NIL NIL))
$$$lang.pvs
memories: THEORY
BEGIN
n: nat = 1000
addrs: TYPE = upto(n)
memory: TYPE = [addrs -> int]
END memories
exprs: DATATYPE
BEGIN
IMPORTING memories
const(n: int): num?
varbl(a: addrs): vbl?
+(x,y: exprs): sum?
-(x,y: exprs): diff?
~(x: exprs): minus?
END exprs
statements: DATATYPE
BEGIN
IMPORTING memories, exprs
assign(a:addrs, e:exprs): assign?
seq(p,q: statements): seq?
ifelse(t: exprs, i,e:statements): ifelse?
for(l: nat, b:statements): for?
END statements
eval: THEORY
BEGIN
IMPORTING statements
valof(v: exprs)(mem: memory): RECURSIVE int =
CASES v OF
const(n): n,
varbl(a): mem(a),
+(x,y): valof(x)(mem) + valof(y)(mem),
-(x,y): valof(x)(mem) - valof(y)(mem),
~(x): - valof(x)(mem)
ENDCASES
MEASURE v BY <<
arb: memory
test1: LEMMA valof(-(const(3), ~(const(4))))(arb) = 7
test2: LEMMA valof(const(3) - ~const(4))(arb) = 7
CONVERSION const
test3: lemma valof(3 - ~4)(arb) = 7
CONVERSION varbl
test4: lemma valof(3 - ~4)(arb) = 7
test4a: lemma valof(3 - ~4)(arb with [(3):=12, (4):=-5]) = 7
% meas(s,t:statements): bool = s << t or
% (for?(s) and for?(t) and b(s)=b(t) and l(s)= runtime(b!1)")
(("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
NIL)
(|exec_TCC6| "" (TERMINATION-TCC)
(("" (LEMMA "nnreal_times_nnreal_is_nnreal")
(("" (INST -1 "l!1-1" "runtime(b!1)") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|exec_TCC7| "" (TERMINATION-TCC) NIL NIL)
(|test5| "" (GRIND) NIL NIL) (|test5a| "" (GRIND) NIL NIL)
(|test_sum_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|test_sum_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|test_sum| "" (BETA *) (("" (GRIND) NIL NIL)) NIL)
(|program_prop_lemma_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|program_prop_lemma_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|program_prop_lemma| "" (INSTALL-REWRITES :DEFS T)
(("" (INDUCT "j")
(("1" (REDUCE) NIL NIL)
("2" (SKOSIMP*)
(("2" (EXPAND "exec" +)
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|program_prop| ""
(GRIND :DEFS EXPLICIT :REWRITES ("program_prop_lemma")) NIL NIL))
$$$expression.pvs
expression: DATATYPE WITH SUBTYPES term, typ
BEGIN
base_type(n:nat): base_type? : typ
funtype(dom: typ, ran: typ): funtype? : typ
variable(n:nat): variable? : term
number(num:nat): number? : term
lam(v: (variable?), ty: typ, ex: term): lam? : term
app(op: term, arg: term): app? : term
END expression
$$$expression.prf
(|elemexpr|)
(|elemeval| (|valof_TCC1| "" (WELL-FOUNDED-TCC))
(|valof_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|valof_TCC3| "" (TERMINATION-TCC) NIL NIL)
(|valof_TCC4| "" (TERMINATION-TCC) NIL NIL)
(|valof_TCC5| "" (TERMINATION-TCC) NIL NIL)
(|valof_TCC6| "" (TERMINATION-TCC) NIL NIL) (|test| "" (GRIND) NIL NIL)
(|test2| "" (GRIND) NIL NIL))
(|expression|)
(|eval| (|valof_TCC1| "" (WELL-FOUNDED-TCC))
(|test| "" (ASSERT) (("" (EXPAND "valof") (("" (PROPAX) NIL NIL)) NIL)) NIL))
$$$bijections.pvs
bijections: THEORY
BEGIN
a,b,x,y: var int
A,B,X,Y: var set[int]
P: var pred[[int,int]]
wiggle(P)(A,B): inductive bool = (empty?(A) and empty?(B)) or
(exists X,Y,a,b: A=add(a,X) and B=add(b,Y) and not member(a,X) and not member(b,Y) and P(a,b) and wiggle(P)(X,Y))
wig_sym: lemma symmetric?(P) => symmetric?(wiggle(P))
wig_tran: lemma transitive?(P) => transitive?(wiggle(P))
END bijections
fermat: theory
begin
a,b,m,n,p: var nat
mod(n,p): below(p)
modax: axiom exists (q:nat): n=q*p+mod(n,p)
prime(p:posnat): bool = forall (x:below(p)): x>1 => mod(p,x)=x
e_lem: lemma prime(p) and mod(a*b,p)=0 => mod(a,p)=0 or mod(b,p)=0
flem: lemma 0 mod(n*a,p) /= mod(m*a,p)
end fermat
$$$bijections.prf
(|bijections|
(|wig_sym| "" (SKOSIMP)
(("" (EXPAND "symmetric?")
(("" (RULE-INDUCT "wiggle")
(("" (SKOSIMP*)
(("" (GROUND)
(("1" (EXPAND "wiggle") (("1" (PROPAX) NIL NIL)) NIL)
("2" (SKOSIMP)
(("2" (EXPAND "wiggle" +)
(("2" (GROUND)
(("1" (INST?)
(("1" (INST?)
(("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL)) NIL))
NIL)
("2" (INST?)
(("2" (INST?)
(("2" (GROUND) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|wig_tran| "" (SKOSIMP)
(("" (EXPAND "transitive?")
(("" (SKOLEM! +)
(("" (FLATTEN)
((""
(LEMMA "bijections.wiggle_weak_induction" :SUBST
(P1
(TYPECHECKED "LAMBDA (x_136: set[int], y_137: set[int]):
wiggle(P!1)(x_136, y!1) AND wiggle(P!1)(y!1, y_137) IMPLIES
wiggle(P!1)(x_136, y_137)" "[[set[int], set[int]] -> boolean]")
P (TYPECHECKED "P!1" "pred[[int, int]]")))
(("" (PROP)
(("1" (INST? :POLARITY? T) (("1" (POSTPONE) NIL NIL)) NIL)
("2" (POSTPONE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
(|fermat|
(|flem| "" (SKOSIMP)
(("" (CASE "mod(a!1*(n!1-m!1),p!1)=0")
(("1" (POSTPONE) NIL NIL)
("2" (LEMMA "modax")
(("2" (INST - _ "p!1")
(("2" (INST-CP - "n!1*a!1")
(("2" (INST-CP - "m!1*a!1")
(("2" (SKOSIMP*) (("2" (POSTPONE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("3" (ASSERT) (("3" (POSTPONE) NIL NIL)) NIL))
NIL))
NIL))
$$$light_bakery.pvs
light_bakery : THEORY
BEGIN
location : type = {idle,entering,critical}
staterec: type = [# pc1, pc2: location, y1,y2 : nat #]
u,v,s,s1,s2,state,state1,state2: var staterec
Q: var pred[staterec]
nextp1(state1,state2):boolean =
IF idle?(pc1(state1)) THEN (state2 = state1 WITH
[(y1) := y2(state1) + 1,
(pc1) := entering])
ELSIF
entering?(pc1(state1)) and
( y2(state1)=0 OR y1(state1) <= y2(state1)) THEN
state2 = state1 WITH [(pc1) := critical]
ELSIF
critical?(pc1(state1)) THEN
(state2 = state1 WITH [(pc1) := idle,(y1) := 0])
ELSE state2 = state1
ENDIF
nextp2(state1,state2):boolean =
IF idle?(pc2(state1)) THEN (state2 = state1 WITH
[(y2) := (y1(state1)) + 1,
(pc2) := entering])
ELSIF entering?(pc2(state1)) and
(y1(state1)=0 OR not(y1(state1) <= y2(state1))) THEN
state2 = state1 WITH [(pc2) := critical]
ELSIF
critical?(pc2(state1)) THEN
(state2 = state1 WITH [(pc2) := idle,(y2) := 0])
ELSE state2 = state1
ENDIF
N(state1,state2):bool =
nextp1(state1,state2) OR
nextp2(state1,state2)
ii(s): bool = idle?(pc1(s)) and idle?(pc2(s))
it(s): bool = idle?(pc1(s)) and entering?(pc2(s)) and y2(s)/=0
ic(s): bool = idle?(pc1(s)) and critical?(pc2(s)) and y2(s)/=0
tc(s): bool = entering?(pc1(s)) and critical?(pc2(s)) and y1(s)/=0 and y2(s)/=0
and y1(s)>y2(s)
tt(s): bool = entering?(pc1(s)) and entering?(pc2(s)) and y1(s)/=0 and y2(s)/=0
ti(s): bool = entering?(pc1(s)) and idle?(pc2(s)) and y1(s)/=0
ci(s): bool = critical?(pc1(s)) and idle?(pc2(s)) and y1(s)/=0
ct(s): bool = critical?(pc1(s)) and entering?(pc2(s)) and y1(s)/=0 and y2(s)/=0
and y1(s)<=y2(s)
ii_to_xx: lemma ii(s1) and N(s1,s2) => it(s2) or ti(s2)
it_to_xx: lemma it(s1) and N(s1,s2) => it(s2) or ic(s2) or tt(s2)
ti_to_xx: lemma ti(s1) and N(s1,s2) => ti(s2) or ci(s2) or tt(s2)
ic_to_xx: lemma ic(s1) and N(s1,s2) => tc(s2) or ii(s2)
ci_to_xx: lemma ci(s1) and N(s1,s2) => ct(s2) or ii(s2)
tt_to_xx: lemma tt(s1) and N(s1,s2) =>
tc(s2) or ct(s2) or tt(s2)
tc_to_ti: lemma tc(s1) and N(s1,s2) => ti(s2) or tc(s2)
ct_to_it: lemma ct(s1) and N(s1,s2) => it(s2) or ct(s2)
reachable(s):bool = ii(s) or it(s) or ti(s) or ic(s) or ci(s) or tt(s)
or tc(s) or ct(s)
r_is_r: lemma reachable(s1) and N(s1,s2) => reachable(s2)
strong(s):bool = ((entering?(pc1(s)) or critical?(pc1(s))) => y1(s)/=0)
and ((entering?(pc2(s)) or critical?(pc2(s))) => y2(s)/=0)
and ((critical?(pc1(s)) and entering?(pc2(s))) => y1(s)<=y2(s))
and ((critical?(pc2(s)) and entering?(pc1(s))) => y1(s)>y2(s))
and not (critical?(pc1(s)) and critical?(pc2(s)))
s_is_s:lemma strong(s1) and N(s1,s2) => strong(s2)
init(state): boolean = idle?(pc1(state)) AND idle?(pc2(state))
AND y1(state)=0 AND y2(state)=0
useful1: THEOREM
init(state) IMPLIES
AG(N, LAMBDA state: (entering?(pc1(state)) or critical?(pc1(state)) => y1(state)/=0))(state)
useful2: THEOREM
init(state) IMPLIES
AG(N, LAMBDA state: (entering?(pc2(state)) or critical?(pc2(state)) => y2(state)/=0))(state)
INV, INIT: var pred[staterec]
R:var pred[[staterec,staterec]]
invariant(INV,INIT,R): bool =
(forall s: INIT(s)=>INV(s))
and forall s1,s2: INV(s1) and R(s1,s2) => INV(s2)
CTLinvariant(INV,INIT,R): bool =
forall s: INIT(s) => AG(R, INV)(s)
equivthm1: theorem invariant(INV,INIT,R) => CTLinvariant(INV,INIT,R)
% following only true of the reachable states
equivthm2: theorem invariant(INV,INIT,R) when CTLinvariant(INV,INIT,R)
N0(state1,state2):bool = true
safe: THEOREM
init(state) IMPLIES
AG(N, LAMBDA state: NOT (critical?(pc1(state)) AND
critical?(pc2(state))))(state)
trans : lemma
N(state1,state2)
zozo : lemma
EF(N, LAMBDA state: (critical?(pc1(state)) AND
critical?(pc2(state))))(state)
% (abs-simp ("lambda(state) :y1(state)=0"
% "lambda(state) :y2(state)=0"
% "lambda(state) :y1(state) <= y2(state)"))
% (abstract ("lambda(state) :y1(state)=0" "lambda(state) :y2(state)=0" "lambda(state) :y1(state) <= y2(state)"))
% (interpret-and-prove ("lambda(state):y1(state)=0" "lambda(state):y2(state)=0" "lambda(state):y1(state)<=y2(state)"))
%
END light_bakery
$$$light_bakery.prf
(light_bakery (ii_to_xx 0 (ii_to_xx-1 nil 3386654193 3386654250 ("" (grind) nil nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (ii const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (/= const-decl "boolean" notequal nil) (it const-decl "bool" light_bakery nil) (ti const-decl "bool" light_bakery nil)) 513 450 nil nil)) (it_to_xx 0 (it_to_xx-1 nil 3386654193 3386654250 ("" (grind) nil nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (it const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (ic const-decl "bool" light_bakery nil) (tt const-decl "bool" light_bakery nil)) 597 500 nil nil)) (ti_to_xx 0 (ti_to_xx-1 nil 3386654193 3386654251 ("" (grind) nil nil) proved ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (/= const-decl "boolean" notequal nil) (ti const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (ci const-decl "bool" light_bakery nil) (tt const-decl "bool" light_bakery nil)) 620 500 nil nil)) (ic_to_xx 0 (ic_to_xx-1 nil 3386654193 3386654251 ("" (grind) nil nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (ic const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (tc const-decl "bool" light_bakery nil) (ii const-decl "bool" light_bakery nil)) 495 440 nil nil)) (ci_to_xx 0 (ci_to_xx-1 nil 3386654193 3386654252 ("" (grind) nil nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (ci const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (ct const-decl "bool" light_bakery nil) (ii const-decl "bool" light_bakery nil)) 503 430 nil nil)) (tt_to_xx 0 (tt_to_xx-1 nil 3386654193 3386654252 ("" (grind) nil nil) proved ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (tt const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (tc const-decl "bool" light_bakery nil) (ct const-decl "bool" light_bakery nil)) 601 500 nil nil)) (tc_to_ti 0 (tc_to_ti-1 nil 3386654193 3386654253 ("" (grind) nil nil) proved ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (tc const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (ti const-decl "bool" light_bakery nil)) 382 310 nil nil)) (ct_to_it 0 (ct_to_it-1 nil 3386654193 3386654253 ("" (grind) nil nil) proved ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (ct const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil) (it const-decl "bool" light_bakery nil)) 370 300 nil nil)) (r_is_r 0 (r_is_r-1 nil 3386654193 3386654256 ("" (grind) nil nil) proved ((odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ii const-decl "bool" light_bakery nil) (/= const-decl "boolean" notequal nil) (it const-decl "bool" light_bakery nil) (ti const-decl "bool" light_bakery nil) (ic const-decl "bool" light_bakery nil) (ci const-decl "bool" light_bakery nil) (tt const-decl "bool" light_bakery nil) (tc const-decl "bool" light_bakery nil) (ct const-decl "bool" light_bakery nil) (reachable const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil)) 2761 2340 nil nil)) (s_is_s 0 (s_is_s-1 nil 3386654193 3386654259 ("" (grind) nil nil) proved ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (/= const-decl "boolean" notequal nil) (strong const-decl "bool" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (N const-decl "bool" light_bakery nil)) 3312 2730 nil nil)) (useful1 0 (useful1-2 "" 3386784381 3386784381 ("" (abstract-and-mc "staterec" "[# pc1, pc2: location, a: bool #]" (("a" "lambda(state): y1(state)=0"))) nil nil) proved nil 37359705 2020 t shostak) (useful1-1 nil 3386654193 3386654259 ("" (abstract-and-mc ("lambda(state) :y1(state)=0")) nil nil) proved ((N const-decl "bool" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (/= const-decl "boolean" notequal nil) (K_conversion const-decl "T1" K_conversion nil) (EX const-decl "bool" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (AG const-decl "pred[state]" ctlops nil) (init const-decl "boolean" light_bakery nil)) 1 0 nil nil)) (useful2 0 (useful2-2 "" 3386788801 3386788801 ("" (abstract-and-mc "staterec" "[# pc1, pc2: location, a: bool #]" (("a" "lambda(state): y2(state)=0"))) nil nil) proved nil 49995 3160 t shostak) (useful2-1 nil 3386654193 3386654259 ("" (abstract-and-mc ("lambda(state) :y2(state)=0")) nil nil) proved ((N const-decl "bool" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (/= const-decl "boolean" notequal nil) (K_conversion const-decl "T1" K_conversion nil) (EX const-decl "bool" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (AG const-decl "pred[state]" ctlops nil) (init const-decl "boolean" light_bakery nil)) 2 0 nil nil)) (equivthm1 0 (equivthm1-1 nil 3386654193 3386654259 ("" (grind :if-match nil) (("" (inst -4 "lambda s: not INV!1(s)") (("" (ground) (("1" (reduce) nil nil) ("2" (skosimp) (("2" (ground) (("2" (skosimp) (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (staterec type-eq-decl nil light_bakery nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (location type-decl nil light_bakery nil) (CTLinvariant const-decl "bool" light_bakery nil) (AG const-decl "pred[state]" ctlops nil) (glb const-decl "pred[T]" mucalculus nil) (member const-decl "bool" sets nil) (EF const-decl "pred[state]" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (mu const-decl "pred[T]" mucalculus nil) (lfp const-decl "pred[T]" mucalculus nil) (<= const-decl "bool" mucalculus nil) (EX const-decl "bool" ctlops nil) (K_conversion const-decl "T1" K_conversion nil) (invariant const-decl "bool" light_bakery nil)) 297 220 nil nil)) (equivthm2 0 (equivthm2-1 nil 3386654193 3386788894 ("" (grind :if-match nil) (("1" (postpone) nil nil) ("2" (inst?) (("2" (ground) (("2" (skosimp) (("2" (reduce) nil nil)) nil)) nil)) nil)) nil) unfinished nil 36846 470 t nil)) (safe 0 (safe-2 "" 3386789402 3386789402 ("" (abstract-and-mc "staterec" "[# pc1, pc2: location, a, b, c: bool #]" (("a" "lambda(state): y1(state)=0") ("b" "lambda(state): y2(state)=0") ("c" "lambda(state): y1(state) <= y2(state)"))) nil nil) proved nil 133809 5570 t shostak) (safe-1 nil 3386654193 3386654260 ("" (abstract-and-mc ("lambda(state) :y1(state)=0" "lambda(state) :y2(state)=0" "lambda(state) :y1(state) <= y2(state)")) nil nil) proved ((N const-decl "bool" light_bakery nil) (nextp2 const-decl "boolean" light_bakery nil) (nextp1 const-decl "boolean" light_bakery nil) (K_conversion const-decl "T1" K_conversion nil) (EX const-decl "bool" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (AG const-decl "pred[state]" ctlops nil) (init const-decl "boolean" light_bakery nil)) 2 0 nil nil)) (trans 0 (trans-2 "" 3386789486 3386789486 ("" (abstract-and-mc "staterec" "[# pc1, pc2: location, a, b, c: bool #]" (("a" "lambda(state): y1(state)=0") ("b" "lambda(state): y2(state)=0") ("c" "lambda(state): y1(state) <= y2(state)"))) (("" (postpone) nil nil)) nil) unfinished nil 55837 4880 t shostak) (trans-1 nil 3386654193 3386654260 ("" (abstract ("lambda(state) :y1(state)=0" "lambda(state) :y2(state)=0" "lambda(state) :y1(state) <= y2(state)")) (("" (postpone) nil)) nil) unfinished nil 3 10 nil nil)) (zozo 0 (zozo-2 "" 3386793585 3386793585 ("" (abstract "staterec" "[# pc1, pc2: location, a, b, c: bool #]" (("a" "lambda(state): y1(state)=0") ("b" "lambda(state): y2(state)=0") ("c" "lambda(state): y1(state) <= y2(state)"))) (("1" (musimp) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst 1 "(# pc1 := astate!1`pc1, pc2 := astate!1`pc2,
y1 := if astate!1`a then 0 else 2 endif,
y2:= if astate!1`b then 0 elsif astate!1`c then 2 else 1 endif #)") (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (ground) nil nil)) nil) ("4" (lift-if) (("4" (ground) (("4" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 2745121 840 t shostak) (zozo-1 nil 3386654193 3386654260 ("" (interpret-and-prove ("lambda(state):y1(state)=0" "lambda(state):y2(state)=0" "lambda(state):y1(state)<=y2(state)")) nil nil) unfinished nil 7 0 nil nil)))
$$$bakery.pvs
bakery: THEORY
BEGIN
phase : TYPE = {idle, trying, critical}
state: TYPE = [# pc1, pc2: phase, t1,t2: nat #]
s, pre, post: VAR state
P1_transition(pre, post): boolean = % pre = post OR
IF pre`pc1 = idle
THEN post = pre WITH [(t1) := pre`t2 + 1, (pc1) := trying]
ELSIF pre`pc1 = trying AND (pre`t2 = 0 OR pre`t1 < pre`t2)
THEN post = pre WITH [(pc1) := critical]
ELSIF pre`pc1 = critical
THEN post = pre WITH [(t1) := 0, (pc1) := idle]
ELSE post = pre
ENDIF
P2_transition(pre, post): boolean = % pre = post OR
IF pre`pc2 = idle
THEN post = pre WITH [(t2) := pre`t1 + 1, (pc2) := trying]
ELSIF pre`pc2 = trying AND (pre`t1 = 0 OR pre`t1 > pre`t2)
THEN post = pre WITH [(pc2) := critical]
ELSIF pre`pc2 = critical
THEN post = pre WITH [(t2) := 0, (pc2) := idle]
ELSE post = pre
ENDIF
transitions(pre, post): bool = P1_transition(pre, post) OR P2_transition(pre, post)
init(s): boolean = s`pc1 = idle AND s`pc2 = idle AND s`t1 = 0 AND s`t2 = 0
safe(s): boolean = NOT (s`pc1 = critical AND s`pc2 = critical)
INV, INIT: var pred[state]
R: VAR pred[[state,state]]
invariant(INV, INIT, R): bool =
(FORALL s: INIT(s) => INV(s))
AND FORALL pre,post: INV(pre) AND R(pre, post) => INV(post)
first_try: LEMMA invariant(safe, init, transitions)
strong_safe(s): bool = safe(s)
AND ((s`pc1 = trying OR s`pc1 = critical) => s`t1 /= 0)
AND ((s`pc2 = trying OR s`pc2 = critical) => s`t2 /= 0)
second_try: LEMMA invariant(strong_safe, init, transitions)
inductive_safe(s): bool = strong_safe(s)
AND ((s`pc1 = critical AND s`pc2 = trying) => s`t1 < s`t2)
AND ((s`pc2 = critical AND s`pc1 = trying) => s`t1 > s`t2)
third_try: LEMMA invariant(inductive_safe, init, transitions)
abstract_state: TYPE =
[# pc1, pc2: phase, t1_is_0, t2_is_0, t1_lt_t2: bool #]
a_s, a_pre, a_post: VAR abstract_state
abst(s): abstract_state =
(# pc1 := s`pc1, pc2 := s`pc2,
t1_is_0 := s`t1 = 0, t2_is_0 := s`t2 = 0,
t1_lt_t2 := s`t1 < s`t2 #)
a_init(a_s): bool =
a_s`pc1 = idle AND a_s`pc2 = idle AND a_s`t1_is_0 AND a_s`t2_is_0
a_safe(a_s): boolean = NOT (a_s`pc1 = critical AND a_s`pc2 = critical)
a_P1_transition(a_pre, a_post): bool = % a_pre = a_post OR
IF a_pre`pc1 = idle
THEN a_post = a_pre WITH [(t1_is_0) := false,
(t1_lt_t2) := false,
(pc1) := trying]
ELSIF a_pre`pc1 = trying AND (a_pre`t2_is_0 OR a_pre`t1_lt_t2)
THEN a_post = a_pre WITH [(pc1) := critical]
ELSIF a_pre`pc1 = critical
THEN a_post = a_pre WITH [(t1_is_0) := true,
(t1_lt_t2) := NOT a_pre`t2_is_0,
(pc1) := idle]
ELSE a_post = a_pre
ENDIF
a_P2_transition(a_pre, a_post): bool = % a_pre = a_post OR
IF a_pre`pc2 = idle
THEN a_post = a_pre WITH [(t2_is_0) := false,
(t1_lt_t2) := true,
(pc2) := trying]
ELSIF a_pre`pc2 = trying AND (a_pre`t1_is_0 OR NOT a_pre`t1_lt_t2)
THEN a_post = a_pre WITH [(pc2) := critical]
ELSIF a_pre`pc2 = critical
THEN a_post = a_pre WITH [(t2_is_0) := true,
(t1_lt_t2) := false,
(pc2) := idle]
ELSE a_post = a_pre
ENDIF
a_trans(a_pre, a_post): bool = a_P1_transition(a_pre, a_post)
OR a_P2_transition(a_pre, a_post)
init_simulation: THEOREM
init(s) IMPLIES a_init(abst(s))
trans_simulation: THEOREM
transitions(pre, post) IMPLIES a_trans(abst(pre), abst(post))
not_eq(s): bool = s`t1 = s`t2 => s`t1=0
extra: LEMMA invariant(not_eq, init, transitions)
strong_trans_simulation: THEOREM
invariant(not_eq, init, transitions) and not_eq(pre) and
not_eq(post) and
transitions(pre, post) IMPLIES a_trans(abst(pre), abst(post))
safety_preserved: THEOREM a_safe(abst(s)) IMPLIES safe(s)
abs_invariant_ctl: THEOREM
a_init(a_s) IMPLIES AG(a_trans, a_safe)(a_s)
auto_abstract: THEOREM init(s) IMPLIES AG(transitions, safe)(s)
END bakery
$$$bakery.prf
(bakery (first_try 0 (first_try-1 nil 3386654193 3386654239 ("" (expand "invariant") (("" (ground) (("1" (grind) nil nil) ("2" (skosimp) (("2" (expand "transitions") (("2" (ground) (("1" (expand "P1_transition") (("1" (ground) (("1" (grind) nil nil) ("2" (grind) (("2" (postpone) nil nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 340 280 nil nil)) (second_try 0 (second_try-1 nil 3386654193 3386654240 ("" (expand "invariant") (("" (ground) (("1" (grind) nil nil) ("2" (skosimp) (("2" (expand "transitions") (("2" (ground) (("1" (expand "P1_transition") (("1" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) (("3" (postpone) nil nil)) nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 501 440 nil nil)) (third_try 0 (third_try-1 nil 3386654193 3386654243 ("" (grind) nil nil) proved ((odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (init const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil) (/= const-decl "boolean" notequal nil) (strong_safe const-decl "bool" bakery nil) (inductive_safe const-decl "bool" bakery nil) (P1_transition const-decl "boolean" bakery nil) (P2_transition const-decl "boolean" bakery nil) (transitions const-decl "bool" bakery nil) (invariant const-decl "bool" bakery nil)) 3223 2670 nil nil)) (init_simulation 0 (init_simulation-1 nil 3386654193 3386654243 ("" (grind) nil nil) proved ((init const-decl "boolean" bakery nil) (abst const-decl "abstract_state" bakery nil) (a_init const-decl "bool" bakery nil)) 69 40 nil nil)) (trans_simulation 0 (trans_simulation-1 nil 3386654193 3386726140 ("" (skosimp) (("" (expand "transitions") (("" (ground) (("1" (expand "P1_transition") (("1" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil)) nil)) nil) ("2" (expand "P2_transition") (("2" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 1067782 1990 t nil)) (extra 0 (extra-1 nil 3386654193 3386654246 ("" (grind) nil nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (init const-decl "boolean" bakery nil) (not_eq const-decl "bool" bakery nil) (P1_transition const-decl "boolean" bakery nil) (P2_transition const-decl "boolean" bakery nil) (transitions const-decl "bool" bakery nil) (invariant const-decl "bool" bakery nil)) 642 560 nil nil)) (strong_trans_simulation 0 (strong_trans_simulation-1 nil 3386654193 3386654249 ("" (skosimp) (("" (expand "transitions") (("" (ground) (("1" (expand "P1_transition") (("1" (apply (then (ground) (grind))) nil nil)) nil) ("2" (expand "P2_transition") (("2" (apply (then (ground) (grind))) nil nil)) nil)) nil)) nil)) nil) proved ((transitions const-decl "bool" bakery nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (P1_transition const-decl "boolean" bakery nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a_trans const-decl "bool" bakery nil) (a_P2_transition const-decl "bool" bakery nil) (a_P1_transition const-decl "bool" bakery nil) (abst const-decl "abstract_state" bakery nil) (invariant const-decl "bool" bakery nil) (not_eq const-decl "bool" bakery nil) (init const-decl "boolean" bakery nil) (P2_transition const-decl "boolean" bakery nil) (state type-eq-decl nil bakery nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phase type-decl nil bakery nil)) 3062 2750 nil nil)) (safety_preserved 0 (safety_preserved-1 nil 3386654193 3386654249 ("" (grind) nil nil) proved ((abst const-decl "abstract_state" bakery nil) (a_safe const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil)) 58 40 nil nil)) (abs_invariant_ctl 0 (abs_invariant_ctl-1 nil 3386654193 3386654249 ("" (model-check) nil nil) proved ((a_init const-decl "bool" bakery nil) (AG const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EX const-decl "bool" ctlops nil) (K_conversion const-decl "T1" K_conversion nil) (a_safe const-decl "boolean" bakery nil) (a_P1_transition const-decl "bool" bakery nil) (a_P2_transition const-decl "bool" bakery nil) (a_trans const-decl "bool" bakery nil)) 275 220 nil nil)) (auto_abstract 0 (auto_abstract-3 "" 3386784603 3386784603 ("" (abstract-and-mc "state" "abstract_state" (("t1_is_0" "lambda (s): s`t1=0") ("t2_is_0" "lambda (s): s`t2=0") ("t1_lt_t2" "lambda(s): s`t1 < s`t2"))) nil nil) proved nil 174099 5910 t shostak) (auto_abstract-2 "" 3386746906 3386746906 ("" (abstract-and-mc "state" "abstract_state" ("lambda (s): s`t1=0" "lambda (s): s`t2=0" "lambda(s): s`t1 < s`t2")) (("" (postpone) nil nil)) nil) proved ((transitions const-decl "bool" bakery nil) (P2_transition const-decl "boolean" bakery nil) (P1_transition const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil) (a_safe const-decl "boolean" bakery nil) (abst const-decl "abstract_state" bakery nil) (K_conversion const-decl "T1" K_conversion nil) (EX const-decl "bool" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (AG const-decl "pred[state]" ctlops nil) (init const-decl "boolean" bakery nil)) 20714435 2340 t shostak) (auto_abstract-1 nil 3386654193 3386654249 ("" (abstract-and-mc ("lambda(s) :s`t1=0" "lambda(s) :s`t2=0" "lambda(s) :s`t1 < s`t2 ")) nil nil) unfinished nil 1 0 nil nil)))
$$$phone_4.pvs
phone_4 : THEORY
BEGIN
N: type = {a,b,c}
P: type = upto(10)
B: TYPE = [N -> setof[P]] % phone books
VB: TYPE = {b:B | (FORALL (x,y:N): x /= y => disjoint?(b(x), b(y)))}
nm, x: VAR N
pn: VAR P
bk: VAR VB
emptybook: VB = (LAMBDA (x:N): emptyset[P])
FindPhone(bk,nm): setof[P] = bk(nm)
UnusedPhoneNum(bk,pn): bool =
(FORALL nm: NOT member(pn,FindPhone(bk,nm)))
AddPhone(bk,nm,pn): VB =
IF UnusedPhoneNum(bk,pn) THEN bk WITH [(nm) := add(pn, bk(nm))]
ELSE bk
ENDIF
DelPhone(bk,nm): VB = bk with [(nm) := emptyset[P]]
DelPhoneNum(bk,nm,pn): VB = bk WITH [(nm) := remove(pn, bk(nm))]
FindAdd: CONJECTURE UnusedPhoneNum(bk,pn) IMPLIES
member(pn,FindPhone(AddPhone(bk,nm,pn),nm))
DelAdd: CONJECTURE DelPhoneNum(AddPhone(bk,nm,pn),nm,pn) =
DelPhoneNum(bk,nm,pn)
END phone_4
phone : THEORY
BEGIN
importing phone_4,print
nm, x: VAR N
pn: VAR P
bk: VAR VB
printset(a:setof[P]) : bool = sprint("{") and
(forall (x:P): if member(x,a) then pvsprint(x,"P") and space else true endif)
and sprint("}")
printbook(bk:VB): bool = terpri and forall (nm:N): pvsprint(nm,"N") and sprint(" : ")
and printset(bk(nm)) and terpri
lift((f: [VB,N,P->VB]),nm,pn): bool =
let bk=read[VB], v=f(bk,nm,pn) in write(v) and printbook(v)
lift((f: [VB,N->VB]),nm): bool =
let bk=read[VB], v=f(bk,nm) in write(v) and printbook(v)
addp(nm,pn): bool = lift(AddPhone,nm,pn)
delp(nm,pn): bool = lift(DelPhoneNum,nm,pn)
delp(nm): bool = lift(DelPhone,nm)
empty: bool = let bk = emptybook in write(bk) and printbook(bk)
findphone(nm): bool = printset(FindPhone(read,nm))
printb: bool = let b=read[VB] in printbook(b)
% addphone(nm,pn): bool = let bk=read[VB], v=AddPhone(bk,nm,pn) in write(v) and printbook(v)
% delphone(nm): bool = let bk=read[VB], v=DelPhone(bk,nm) in write(v) and printbook(v)
% delphonenum(nm,pn): bool = let bk=read[VB], v=DelPhoneNum(bk,nm,pn) in write(v) and printbook(v)
end phone
$$$phone_4.prf
(|phone_4| (|emptybook_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|AddPhone_TCC1| "" (GRIND :IF-MATCH NIL)
(("1" (INST - "x!1" "y!1") (("1" (REDUCE) NIL NIL)) NIL)
("2" (INST - "x!1" "y!1") (("2" (REDUCE) NIL NIL)) NIL)
("3" (INST - "x!1" "y!1") (("3" (REDUCE) NIL NIL)) NIL)
("4" (INST - "x!1" "y!1") (("4" (REDUCE) NIL NIL)) NIL)
("5" (INST - "x!1" "y!1") (("5" (REDUCE) NIL NIL)) NIL))
NIL)
(|DelPhone_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|DelPhoneNum_TCC1| "" (GRIND :IF-MATCH NIL)
(("1" (INST - "x!1" "y!1") (("1" (REDUCE) NIL NIL)) NIL)
("2" (INST - "x!1" "y!1") (("2" (REDUCE) NIL NIL)) NIL)
("3" (INST - "x!1" "y!1") (("3" (REDUCE) NIL NIL)) NIL))
NIL)
(|FindAdd| "" (GRIND) NIL NIL)
(|DelAdd| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T)
(("" (SMASH)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (BDDSIMP) NIL NIL))
NIL))
NIL))
NIL))
NIL))
$$$phone_3.pvs
phone_3 : THEORY
BEGIN
N: TYPE % names
P: TYPE % phone numbers
B: TYPE = [N -> setof[P]] % phone books
nm, x: VAR N
pn: VAR P
bk: VAR B
emptybook(nm): setof[P] = emptyset[P]
FindPhone(bk, nm): setof[P] = bk(nm)
AddPhone(bk, nm, pn): B = bk WITH [(nm) := add(pn, bk(nm))]
DelPhone(bk,nm): B = bk WITH [(nm) := emptyset[P]]
DelPhoneNum(bk,nm,pn): B = bk WITH [(nm) := remove(pn, bk(nm))]
FindAdd: CONJECTURE member(pn, FindPhone(AddPhone(bk, nm, pn), nm))
DelAdd: CONJECTURE DelPhoneNum(AddPhone(bk, nm, pn), nm, pn) =
DelPhoneNum(bk, nm, pn)
updates: VAR list[[N, P]]
AddList(bk, updates): RECURSIVE B =
CASES updates OF
null: bk,
cons(upd, rest): AddList(AddPhone(bk, proj_1(upd), proj_2(upd)), rest)
ENDCASES
MEASURE length(updates)
AddList_member: CONJECTURE
member(pn, FindPhone(bk, nm)) =>
member(pn, FindPhone(AddList(bk, updates), nm))
FindList: CONJECTURE
(every! (upd:[N, P]): proj_1(upd)/=nm) (updates) =>
FindPhone(AddList(bk, updates), nm) = FindPhone(bk, nm)
END phone_3
$$$phone_3.prf
(|phone_3| (|FindAdd| "" (GRIND) NIL)
(|DelAdd| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T)
(("" (SMASH)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (SMASH) NIL)))))))))
(|AddList_TCC1| "" (TERMINATION-TCC) NIL)
(|AddList_member| "" (INDUCT-AND-SIMPLIFY "updates") NIL)
(|FindList| "" (INDUCT-AND-SIMPLIFY "updates") NIL))
$$$phone_2.pvs
phone_2: THEORY
BEGIN
N: NONEMPTY_TYPE % names
P: NONEMPTY_TYPE % phone numbers
B: TYPE = [N -> P] % phone books
n0: P
GP: TYPE = {pn: P | pn /= n0}
nm: VAR N
a_name: N
pn: VAR P
bk: VAR B
gp, gp1, gp2: VAR GP
emptybook(nm): P = n0
FindPhone(bk, nm): P = bk(nm)
Known?(bk, nm): bool = bk(nm) /= n0
AddPhone(bk, nm, gp): B =
IF Known?(bk, nm) THEN bk ELSE bk WITH [(nm) := gp] ENDIF
ChangePhone(bk, nm, gp): B =
IF Known?(bk, nm) THEN bk WITH [(nm) := gp] ELSE bk ENDIF
DelPhone(bk, nm): B = bk WITH [(nm) := n0]
FindAdd: CONJECTURE
NOT Known?(bk, nm) => FindPhone(AddPhone(bk, nm, gp), nm) = gp
whoops: AXIOM Known?(AddPhone(bk, nm, pn), nm)
aargh: LEMMA true=false
whoops_corrected: AXIOM Known?(AddPhone(bk, nm, gp), nm)
FindChange: CONJECTURE
Known?(bk, nm) => FindPhone(ChangePhone(bk, nm, gp), nm) = gp
DelAdd: CONJECTURE
DelPhone(AddPhone(bk, nm, gp), nm) = DelPhone (bk, nm)
KnownAdd: CONJECTURE Known?(AddPhone(bk, nm, gp), nm)
AddChange: CONJECTURE
ChangePhone(AddPhone(bk, nm, gp1), nm, gp2) =
AddPhone(ChangePhone(bk, nm, gp2), nm, gp2)
END phone_2
$$$phone_2.prf
(|phone_2|
(|FindAdd| "" (SKOSIMP)
(("" (EXPAND "Known?")
(("" (EXPAND "FindPhone")
(("" (EXPAND "AddPhone")
(("" (EXPAND "Known?")
(("" (LIFT-IF)
(("" (SPLIT)
(("1" (FLATTEN) NIL NIL) ("2" (PROPAX) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|whoops_TCC1| "" (SUBTYPE-TCC))
(|aargh| "" (LEMMA "whoops")
(("" (INST -1 _ _ "n0")
(("" (INST -1 "emptybook" _)
(("" (INST -1 "a_name")
(("" (EXPAND "Known?") (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|whoops_corrected| "" (GRIND) NIL NIL)
(|FindChange| "" (GRIND) NIL NIL) (|DelAdd| "" (GRIND) NIL NIL)
(|KnownAdd| "" (GRIND) NIL NIL) (|AddChange| "" (GRIND) NIL NIL))
$$$phone_1.pvs
phone_1: THEORY
BEGIN
N: TYPE % names
P: NONEMPTY_TYPE % phone numbers
B: TYPE = [N -> P] % phone books
n0: P
emptybook: B
emptyax: AXIOM FORALL (nm: N): emptybook(nm) = n0
FindPhone: [B, N -> P]
Findax: AXIOM FORALL (bk: B), (nm: N): FindPhone(bk, nm) = bk(nm)
AddPhone: [B, N, P -> B]
Addax: AXIOM FORALL (bk: B), (nm: N), (pn: P):
AddPhone(bk, nm, pn) = bk WITH [(nm) := pn]
FindAdd: CONJECTURE FORALL (bk: B), (nm: N), (pn: P):
FindPhone(AddPhone(bk, nm, pn), nm) = pn
DelPhone: [B, N -> B]
Delax: AXIOM FORALL (bk: B), (nm: N):
DelPhone(bk, nm) = bk WITH [(nm) := n0]
DelAdd: CONJECTURE FORALL (bk: B), (nm: N), (pn: P):
DelPhone(AddPhone(bk, nm, pn), nm) = bk
DelAdd2: CONJECTURE FORALL (bk: B), (nm: N), (pn: P):
FindPhone(bk, nm) = n0 => DelPhone(AddPhone(bk, nm, pn), nm) = bk
DelAdd3: CONJECTURE FORALL (bk: B), (nm: N), (pn: P):
DelPhone(AddPhone(bk, nm, pn), nm) = DelPhone(bk, nm)
KnownAdd: CONJECTURE FORALL (bk: B), (nm: N), (pn: P):
FindPhone(AddPhone(bk, nm, pn), nm) /= n0
END phone_1
$$$phone_1.prf
(|phone_1| (|FindAdd| "" (GRIND :THEORIES ("phone_1")) NIL)
(|DelAdd| "" (GRIND :THEORIES ("phone_1"))
(("" (APPLY-EXTENSIONALITY)
(("" (DELETE 2)
(("" (LIFT-IF) (("" (GROUND) (("" (POSTPONE) NIL)))))))))))
(|DelAdd2| "" (GRIND :THEORIES ("phone_1"))
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (SMASH) NIL)))))
(|DelAdd3| "" (GRIND :THEORIES ("phone_1")) NIL)
(|KnownAdd| "" (GRIND :THEORIES ("phone_1")) (("" (POSTPONE) NIL))))
$$$phones.pvs
phones: THEORY
BEGIN
IMPORTING phone_1, phone_2, phone_3, phone_4
END phones
$$$phones.prf
(|phones|)