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.
%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))))