PVS dump file simple_tables.dmp
To extract the specifications and proofs, download this file to
simple_tables.dmp and from a running PVS type the command
M-x undump-pvs-files
You will be prompted for the dump file name (simple_tables.dmp) and the
directory in which to dump the extracted files.
<![CDATA[
%Patch files loaded: (patch2-test patch2) version 2.377
$$$simple_tables.pvs
simple_tables: THEORY
BEGIN
signs: TYPE = { x: int | x >= -1 & x <= 1}
x: var int
sign_traditional(x): signs = IF x<0 THEN -1 ELSIF x>0 then 1 ELSE 0 ENDIF
sign_cond(x): signs =
COND
x<0 -> -1,
x=0 -> 0,
x>0 -> 1
ENDCOND
sign_cond2(x): signs =
COND
x<0 -> -1,
x=0 -> 0,
ELSE -> 1
ENDCOND
trad_cond_same: LEMMA sign_traditional = sign_cond
trad_cond2_same: LEMMA sign_traditional = sign_cond2
sign_vtable(x): signs = TABLE
%----------%
| x<0 | -1 ||
%----------%
| x=0 | 0 ||
%----------%
| x>0 | 1 ||
%----------%
ENDTABLE
sign_vtable2(x): signs = TABLE
%----------%
| x<0 | -1 ||
%----------%
| x=0 | 0 ||
%----------%
| ELSE| 1 ||
%----------%
ENDTABLE
sign_htable(x): signs = TABLE
%-------------------%
|[ x<0 | x=0 | x>0 ]|
%-------------------%
| -1 | 0 | 1 ||
%-------------------%
ENDTABLE
sign_htable2(x): signs = TABLE
%-------------------%
|[ x<0 | x=0 | ELSE ]|
%-------------------%
| -1 | 0 | 1 ||
%-------------------%
ENDTABLE
trad_vtable_same: LEMMA sign_traditional = sign_vtable
trad_htable_same: LEMMA sign_traditional = sign_htable
vtables_same: LEMMA sign_vtable = sign_vtable2
htables_same: LEMMA sign_htable = sign_htable2
calculate: LEMMA sign_htable(-x) = - sign_htable(x)
few_ints: TYPE = { x : int | x >= -2 & x <= 2}
sign_fewh(z:few_ints): signs = TABLE
%---------------------------------%
|[ z = -2 | z = -1 | z = 0 | ELSE ]|
%---------------------------------%
| -1 | -1 | 0 | 1 ||
%---------------------------------%
ENDTABLE
sign_fewh_enum(z:few_ints): signs = TABLE
%---------------------------------%
,z |[ -2 | -1 | 0 | ELSE ]|
%---------------------------------%
| -1 | -1 | 0 | 1 ||
%----------------------------------%
ENDTABLE
sign_fewv_enum(z:few_ints): signs = TABLE
z
%---------%
| -2 | -1 ||
%---------%
| -1 | -1 ||
%---------%
| 0 | 0 ||
%---------%
|ELSE| 1 ||
%---------%
ENDTABLE
h_enum_same: LEMMA sign_fewh = sign_fewh_enum
v_enum_same: LEMMA sign_fewh = sign_fewv_enum
END simple_tables
adt_tables: THEORY
BEGIN
modes: TYPE = { off, armed, engaged }
value(m:modes):bool = TABLE
m
%-----------------%
| off | false ||
%-----------------%
| armed | true ||
%-----------------%
| engaged | true ||
%-----------------%
ENDTABLE
value_alt(m:modes):bool = TABLE
%---------------------%
| off?(m) | false ||
%---------------------%
| armed?(m) | true ||
%---------------------%
| engaged?(m) | true ||
%---------------------%
ENDTABLE
same: LEMMA value = value_alt
END adt_tables
Parnas_examples: THEORY
BEGIN
sqrt: [nonneg_real -> nonneg_real]
Vector_0(x:real): [real, real] =
COND x<0 -> (x+2, 5+sqrt(-x)),
x=0 -> (x+4+(21/100), x-4),
x>0 -> (5+(4/10)+sqrt(x), x)
ENDCOND
Vector_1(x:real): [real, real] =
TABLE
%-----------------------------------------------------------------%
|[ x<0 | x=0 | x>0 ]|
%-----------------------------------------------------------------%
|(x+2, 5+sqrt(-x)) | (x+4+(21/100), x-4) | (5+(4/10)+sqrt(x), x) ||
%-----------------------------------------------------------------%
ENDTABLE
Vector_2(x:real): [real, real] =
TABLE
%------------------------------%
| x<0 | (x+2, 5+sqrt(-x)) ||
%------------------------------%
| x=0 | (x+4+(21/100), x-4) ||
%------------------------------%
| x>0 | (5+(4/10)+sqrt(x), x) ||
%------------------------------%
ENDTABLE
test0_1: LEMMA Vector_0 = Vector_1
test1_2: LEMMA Vector_1 = Vector_2
test_a: LEMMA proj_2(Vector_0(17)) = 17
test_b: LEMMA proj_2(Vector_1(0)) = -4
test_c: LEMMA FORALL (x:real): x/=0 => proj_2(Vector_2(x)) > 0
test_d: LEMMA FORALL (x:real): x > -2 => proj_1(Vector_2(x)) > 0
END Parnas_examples
two_d_tables: THEORY
BEGIN
IMPORTING Parnas_examples
normal2(y,x:real):real =
TABLE
%--------------------------------------------------%
|[ y=27 | y>27 | y<27 ]|
%--------------------------------------------------------%
| x=3 | 27+sqrt(27) | 54+sqrt(27) | y^2 +3 ||
%--------------------------------------------------------%
| x<3 | 27+sqrt(-(x-4)) | y+sqrt(-(x-5)) | y^2 + (x-3)^2 ||
%--------------------------------------------------------%
| x>3 | 27+sqrt(x-3) | 2*y+sqrt(x-3) | y^2 + (3-x)^2 ||
%--------------------------------------------------------%
ENDTABLE
END two_d_tables
blank_entries: THEORY
BEGIN
subp((i: int), (j: {x: int | x <=i })): RECURSIVE nat =
TABLE
%-----|-----------------%
| i=j | 0 ||
%-----|-----------------%
| i>j | subp(i, j+1)+1 ||
%-----|-----------------%
ENDTABLE
MEASURE i-j
subp_blank((i: int), (j: {x: int | x <=i })): RECURSIVE nat =
TABLE
%-----|-----------------------%
| i<j | ||
%-----|-----------------------%
| i=j | 0 ||
%-----|-----------------------%
| i>j | subp_blank(i, j+1)+1 ||
%-----|-----------------------%
ENDTABLE
MEASURE i-j
subp_blank2((i: int), (j: {x: int | x <=i })): RECURSIVE nat =
TABLE
%-----|------------------------%
| i<j | ||
%-----|------------------------%
| i=j | 0 ||
%-----|------------------------%
|ELSE | subp_blank2(i, j+1)+1 ||
%-----|------------------------%
ENDTABLE
MEASURE i-j
bad_subp((i: int), (j: {x: int | x <=i })): RECURSIVE nat =
TABLE
%-----|---------------------%
| i<j | 0 ||
%-----|---------------------%
| i=j | ||
%-----|---------------------%
| i>j | bad_subp(i, j+1)+1 ||
%-----|---------------------%
ENDTABLE
MEASURE i-j
bang: CLAIM bad_subp(3, 3) = 99
END blank_entries
$$$simple_tables.prf
(|simple_tables| (|sign_traditional_TCC1| "" (SUBTYPE-TCC) NIL)
(|sign_traditional_TCC2| "" (SUBTYPE-TCC) NIL)
(|sign_traditional_TCC3| "" (SUBTYPE-TCC) NIL)
(|sign_cond_TCC1| "" (SUBTYPE-TCC) NIL)
(|sign_cond_TCC2| "" (COND-DISJOINT-TCC) NIL)
(|sign_cond_TCC3| "" (COND-COVERAGE-TCC) NIL)
(|sign_cond_TCC4| "" (COND-COVERAGE-TCC) NIL)
(|sign_cond2_TCC1| "" (SUBTYPE-TCC) NIL)
(|sign_cond2_TCC2| "" (COND-DISJOINT-TCC) NIL)
(|trad_cond_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|trad_cond2_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|trad_vtable_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|trad_htable_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|vtables_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|htables_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|calculate| "" (GRIND) NIL) (|sign_fewh_TCC1| "" (SUBTYPE-TCC) NIL)
(|sign_fewh_TCC2| "" (SUBTYPE-TCC) NIL)
(|sign_fewh_TCC3| "" (SUBTYPE-TCC) NIL)
(|sign_fewh_TCC4| "" (SUBTYPE-TCC) NIL)
(|sign_fewh_TCC5| "" (COND-DISJOINT-TCC) NIL)
(|h_enum_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
(|v_enum_same| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))(|adt_tables|
(|value_alt_TCC1|
""
(GRIND)
NIL)
(|value_alt_TCC2|
""
(GRIND)
NIL)
(|same|
""
(APPLY-EXTENSIONALITY
:HIDE?
T)
((""
(GRIND)
NIL))))(|Parnas_examples|
(|Vector_0_TCC1|
""
(SUBTYPE-TCC)
NIL)
(|Vector_0_TCC2|
""
(SUBTYPE-TCC)
NIL)
(|Vector_0_TCC3|
""
(COND-DISJOINT-TCC)
NIL)
(|Vector_0_TCC4|
""
(COND-COVERAGE-TCC)
NIL)
(|test0_1|
""
(APPLY-EXTENSIONALITY
:HIDE?
T)
((""
(GRIND)
NIL)))
(|test1_2|
""
(APPLY-EXTENSIONALITY
:HIDE?
T)
((""
(GRIND)
NIL)))
(|test_a|
""
(GRIND)
NIL)
(|test_b|
""
(GRIND)
NIL)
(|test_c|
""
(GRIND)
NIL)
(|test_d|
""
(GRIND)
NIL))(|two_d_tables|
(|normal2_TCC1|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC2|
""
(COND-DISJOINT-TCC)
NIL)
(|normal2_TCC3|
""
(COND-COVERAGE-TCC)
NIL)
(|normal2_TCC4|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC5|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC6|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC7|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC8|
""
(COND-DISJOINT-TCC)
NIL)
(|normal2_TCC9|
""
(COND-COVERAGE-TCC)
NIL)
(|normal2_TCC10|
""
(SUBTYPE-TCC)
NIL)
(|normal2_TCC11|
""
(COND-DISJOINT-TCC)
NIL)
(|normal2_TCC12|
""
(COND-COVERAGE-TCC)
NIL)
(|normal2_TCC13|
""
(COND-DISJOINT-TCC)
NIL)
(|normal2_TCC14|
""
(COND-COVERAGE-TCC)
NIL))(|blank_entries|
(|subp_TCC1|
""
(SUBTYPE-TCC)
NIL)
(|subp_TCC2|
""
(SUBTYPE-TCC)
NIL)
(|subp_TCC3|
""
(TERMINATION-TCC)
NIL)
(|subp_TCC4|
""
(COND-DISJOINT-TCC)
NIL)
(|subp_TCC5|
""
(COND-COVERAGE-TCC)
NIL)
(|subp_blank2_TCC1|
""
(SUBTYPE-TCC)
NIL)
(|subp_blank2_TCC2|
""
(TERMINATION-TCC)
NIL)
(|subp_blank2_TCC3|
""
(COND-COVERAGE-TCC)
NIL)
(|bad_subp_TCC1|
""
(COND-DISJOINT-TCC)
NIL)
(|bad_subp_TCC2|
""
(COND-COVERAGE-TCC))
(|bang_TCC1|
""
(SUBTYPE-TCC)
NIL)
(|bang|
""
(EXPAND
"bad_subp")
((""
(POSTPONE)
NIL))))
]]>