PVS_theories/fp_lemmas.pvs

+fp_lemmas
+ [b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i}]:THEORY
+
+BEGIN
+
+
+IMPORTING float@IEEE_854_defs[b,p,alpha,E_max,E_min]
+
+infinite_not_zero: LEMMA FORALL (x:fp_num): infinite?(x) => NOT zero?(x)
+
+%finite_mul_1: LEMMA FORALL(x:{fp:fp_num|finite?(fp)},mode:rounding_mode): finite?(fp_mul(x,real_to_fp(1),mode))
+
+op_fin_inf: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp)}, y:{fp:fp_num| finite?(fp)},op:{op:fp_ops|zero?(y) OR (zero?(x) AND zero?(y)) => NOT div?(op)}):
+finite?(fp_op(op,x,y,mode)) OR infinite?(fp_op(op,x,y,mode))
+
+op_add_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): infinite?(x) XOR infinite?(y) => finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(y,x,mode)) OR infinite?(fp_add(y,x,mode)) 
+
+op_sub_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(x,y,mode)) OR infinite?(fp_sub(x,y,mode)) 
+
+op_sub_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(y,x,mode)) OR infinite?(fp_sub(y,x,mode))
+
+op_mul_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(y,x,mode)) OR infinite?(fp_mul(y,x,mode))
+
+op_mul_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(x,y,mode)) OR infinite?(fp_mul(x,y,mode))
+
+op_div_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND NOT zero?(fp)}): finite?(fp_div(x,y,mode)) OR infinite?(fp_div(x,y,mode))
+
+op_div_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) AND NOT zero?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): finite?(fp_div(y,x,mode)) OR infinite?(fp_div(y,x,mode))
+
+op_sqrt_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|(finite?(fp) AND sign(fp) = pos) OR (infinite?(fp) AND i_sign(fp) = pos)}): finite?(fp_sqrt(x,mode)) OR infinite?(fp_sqrt(x,mode))
+
+
+END fp_lemmas

PVS_theories/overload.prf

+(overload
+ (lessp_TCC1 0
+  (lessp_TCC1-1 nil 3508513172 3508513284
+   ("" (skolem!) (("" (grind) nil nil)) nil) proved
+   ((posrat_exp application-judgement "posrat" exponentiation nil)
+    (nnrat_exp application-judgement "nnrat" exponentiation nil)
+    (minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (minus_real_is_real application-judgement "real" reals nil)
+    (real_to_fp const-decl "fp_num" real_to_fp "float/")
+    (number nonempty-type-decl nil numbers nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (numfield nonempty-type-eq-decl nil number_fields nil)
+    (- const-decl "[numfield -> numfield]" number_fields nil)
+    (sign_of const-decl "sign_rep" fp_round_aux "float/")
+    (pos const-decl "sign_rep" enumerated_type_defs "float/")
+    (neg const-decl "sign_rep" enumerated_type_defs "float/")
+    (^ const-decl "real" exponentiation nil)
+    (expt def-decl "real" exponentiation nil)
+    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
+         nil)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (posint_exp application-judgement "posint" exponentiation nil)
+    (posint_plus_nnint_is_posint application-judgement "posint"
+     integers nil)
+    (odd_plus_odd_is_even application-judgement "even_int" integers
+     nil)
+    (posnat_expt application-judgement "posnat" exponentiation nil)
+    (posrat_div_posrat_is_posrat application-judgement "posrat"
+     rationals nil)
+    (posint_times_posint_is_posint application-judgement "posint"
+     integers nil)
+    (even_times_int_is_even application-judgement "even_int" integers
+     nil)
+    (mult_divides1 application-judgement "(divides(n))" divides nil)
+    (mult_divides2 application-judgement "(divides(m))" divides nil)
+    (even_minus_odd_is_odd application-judgement "odd_int" integers
+     nil)
+    (odd_minus_odd_is_even application-judgement "even_int" integers
+     nil)
+    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
+    (minus_even_is_even application-judgement "even_int" integers nil))
+   18355 5670 t nil))
+ (expt_TCC1 0
+  (expt_TCC1-1 nil 3508513172 3508513172 ("" (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))
+   17 20 nil nil))
+ (expt_TCC2 0
+  (expt_TCC2-1 nil 3508513172 3508513172 ("" (termination-tcc) nil nil)
+   proved nil 6 0 nil nil))
+ (caret_TCC1 0
+  (caret_TCC1-1 nil 3508513172 3508513172 ("" (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)
+    (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)
+    (minus_int_is_int application-judgement "int" integers nil)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil))
+   16 20 nil nil)))
+

PVS_theories/overload.pvs

+overload[b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i},
+(IMPORTING float@enumerated_type_defs)r_mode:rounding_mode]:THEORY
+
+BEGIN
+
+IMPORTING fp_lemmas[b,p,alpha,E_max,E_min]
+
+x,y: VAR fp_num
+n:VAR nat
+
+-(x,y):fp_num = fp_sub(x,y,r_mode);
++(x,y):fp_num = fp_add(x,y,r_mode);
+*(x,y):fp_num = fp_mul(x,y,r_mode);
+/(x,y):fp_num = fp_div(x,y,r_mode);
+sqrt(x):fp_num = fp_sqrt(x,r_mode);
+-(x):fp_num = toggle_sign(x);
+
+-(x:fp_num,y:real):fp_num = x-real_to_fp(y);
++(x:fp_num,y:real):fp_num = x+real_to_fp(y);
+*(x:fp_num,y:real):fp_num = x*real_to_fp(y);
+/(x:fp_num,y:real):fp_num = x/real_to_fp(y);
+
+-(x:real,y:fp_num):fp_num = real_to_fp(x)-y;
++(x:real,y:fp_num):fp_num = real_to_fp(x)+y;
+*(x:real,y:fp_num):fp_num = real_to_fp(x)*y;
+/(x:real,y:fp_num):fp_num = real_to_fp(x)/y;
+
+
+<(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) < n_value(y);
+<=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) <= n_value(y);
+>(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) > n_value(y);
+>=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) >= n_value(y);
+=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) = n_value(y);
+/=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) /= n_value(y);
+
+<(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) < y;
+<=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) <= y;
+>(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) > y;
+>=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) >= y;
+=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) = y;
+/=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) /= y;
+
+<(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x < real_to_fp(y);
+<=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x <= real_to_fp(y);
+>(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x > real_to_fp(y);
+>=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x >= real_to_fp(y);
+=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x = real_to_fp(y);
+/=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x /= real_to_fp(y);
+
+expt(x,n): RECURSIVE fp_num =
+  IF n = 0 THEN real_to_fp(1)
+  ELSE x * expt(x, n-1)
+  ENDIF
+MEASURE n;
+
+^(x: fp_num, i:int): fp_num
+    = IF i >= 0 THEN expt(x, i) ELSE real_to_fp(1)/expt(x, -i) ENDIF
+END overload

PVS_theories/single.pvs

+single: THEORY
+
+BEGIN
+ 
+IMPORTING float@enumerated_type_defs
+IMPORTING overload[2,24,192,127,-126,to_nearest]
+
+single: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)}
+single_finite: TYPE = {fp:fp_num|finite?(fp)}
+
+END single

README.txt

-Table Toolbox
+Tabular Expression Toolbox Version 0.7.4
 
 Installation
-Unzip contents and add to folder on matlab path.
+============
 
-See included help files for detailed documentation.
+Unzip contents and add the folder on your matlab path via menu options:
 
-All code (c) Colin Eles, McMaster Center for Software Certification, 2010.
+File -> Set Path.
 
-Contact elesc (at) mcmaster.ca
\ No newline at end of file
+See included help files for detailed documentation or go to
+
+http://www.cas.mcmaster.ca/~lawford/TET
+
+All code copyright: 
+Colin Eles, McMaster Centre for Software Certification, 2011.
+Matthew Dawson, McMaster Centre for Software Certification, 2012-2014.
+
+For more information about the Tabular Expression Toolbox contact: 
+Professor Mark Lawford
+Associate Director
+McMaster Centre for Software Certification
+lawford (at) mcmaster.ca

TTdiag.m

@@ -14,7 +14,7 @@ switch Action,
         Mode = varargin{2};
         
         if 2 ~= nargin
-            DAStudio.warning('improper function use')
+            DAStudio.warning('improper function use');
         end
         blockHandleTTTopMask = orig_gcbh;
         switch Mode,
@@ -35,18 +35,18 @@ switch Action,
         
     case 'Load',
         if 2 ~= nargin
-            DAStudio.warning('improper function use')
+            DAStudio.warning('improper function use');
         end
         file = varargin{2};
         try
             data = importdata(file);
             gui = GUI([],0);
-            gui.setData(data)
+            gui.setData(data);
             gui.init();
         catch exception
-            msgbox(exception.identifier)
+            msgbox(exception.identifier);
         end
-    case 'Delete'
+    case 'Delete',
         blockHandleTTTopMask = orig_gcbh;
         data = get_param(blockHandleTTTopMask,'UserData');
         if isempty(data)
@@ -55,12 +55,12 @@ switch Action,
         if ~data.valid
             errordlg(...
                 DAStudio.message('Block Data has been corputed'),...
-                'Error', 'modal')
+                'Error', 'modal');
             return
         end
         
         if data.open && ishandle(data.fig)
-            delete(data.fig)
+            delete(data.fig);
             data.fig = [];
             data.open = 0;
             set_param(blockHandleTTTopMask,'UserData',data);
@@ -83,7 +83,7 @@ data = get(blockHandleTTTopMask,'UserData');
 if(~isempty(data))
     data_new = data.clone(blockHandleTTTopMask);
     
-    set_param(blockHandleTTTopMask,'UserData',data_new)
+    set_param(blockHandleTTTopMask,'UserData',data_new);
 end
 end
 
@@ -94,12 +94,11 @@ if (mode == 1)
     
     
     % check if the user is trying to open the block from the library
-    if strcmp(get_param(modelHandle,'Lock'), 'on') || ...
-            strcmp(get_param(blockHandleTTTopMask,'LinkStatus'),'implicit')
+    if strcmp(get_param(modelHandle,'Lock'), 'on') || strcmp(get_param(blockHandleTTTopMask,'LinkStatus'),'implicit')
         
         errordlg(...
             DAStudio.message('can not open Model Locked, Add to new model to use'),...
-            'Error', 'modal')
+            'Error', 'modal');
         return
     end
     
@@ -116,15 +115,16 @@ else
     if ~data.valid
         errordlg(...
             DAStudio.message('Block Data has been corputed'),...
-            'Error', 'modal')
+            'Error', 'modal');
         return
     end
     if data.open
         if ishghandle(data.fig)
-            figure(data.fig)
-            
+            figure(data.fig);
+            return            
         end
-        return
+    else
+        data.upgrade
     end
     
 end
@@ -134,7 +134,7 @@ elseif mode == 0
     gui = GUI([],0);
 end
 
-gui.setData(data)
+gui.setData(data);
 gui.init();
 if(mode == 1)
     set_param(blockHandleTTTopMask,'UserData',data);
@@ -153,7 +153,7 @@ data = get_param(blockHandleTTTopMask,'UserData');
 
 if ~isempty(data)
     if data.open
-        delete(data.fig)
+        delete(data.fig);
     end
 end
 %set_param(gui.fig,'Visible','off')

Tests/testEMLGenerator.m

@@ -79,7 +79,7 @@ function testcode_gen
     assertEqual(code,sprintf('function output = test(x)\n%%%%#eml\noutput=(1);\nif(x+1<2)\n  output = (1);\nelseif(x-1>6)\n  output = (2);\nend\n'));
 
     
-    d.Grid2.new_Cell
+    d.Grid2.new_Cell;
     d.Grid2.cells(1).cond_text = 'x+1<2';
     d.Grid2.cells(2).cond_text = 'x-1>6';
     d.Grid1.cells(1).cond_text = 'y<1';

check_system.m

@@ -18,7 +18,7 @@ for i = 1:size(blocks,1)
                 msg = [msg char(blocks(i)) ' is not valid' sprintf('\n')];
             end
             block_data.checked = check;
-            TableBlock.set_block_display(char(blocks(i)),block_data.checked)
+            TableBlock.set_block_display(char(blocks(i)),block_data.checked);
             
         end
     end

html/TT_gs_over.m

@@ -91,7 +91,7 @@ end
 %%
 % Consider our example table, the designer of this table has failed to
 % consider the case when x is equal to 1, the completness condition is not
-% satisfied. Clicking on the PVS button will start the proof and popup a
+% satisfied. Clicking on the Typecheck button will start the proof and popup a
 % process dialog as shown below:
 %
 % <<walk7.png>>
@@ -99,7 +99,9 @@ end
 % If the proof fails it will pop up a dialog giving the user some feedback
 % of why the proof failed as seen in the next image.
 %
-% <<walk8.png>>
+% <<walk8_p1.png>>
+%
+% <<walk8_p2.png>>
 %
 % The Typecheck summary window will display the formula for which a proof
 % was not found. If a proof fails PVS attempts to find a counter example.
@@ -112,7 +114,9 @@ end
 % false for the counter example indicating to the table designer that they
 % failed to consider a case of the input.
 %
-% <<walk9.png>>
+% <<walk9_p1.png>>
+%
+% <<walk9_p2.png>>
 % 
 % In the example above, the designer of the table has captured the case
 % where x = 0 in both conditions of the table. The tool has highlighted

html/TT_gs_ref.m

 %% Tabular Expressions References
+%% Tabular Expression Toolbox Publications
+% * C. Eles and M. Lawford, "A tabular expression toolbox for Matlab/Simulink," NASA Formal Methods, LNCS Vol. 6617, pp. 494-499, Springer, 2011.
 %% Background Information
 % Tabular Expressions have been around for many years, below are some
 % papers discussing some of the fundamentals behind tabular expressions.
 %
-% * Y. Jin and D. L. Parnas, "Defining the meaning of tabular mathematical
-% expressions," Science of Computer Programming, vol. In Press, Corrected Proof, 2010.
+% * Y. Jin and D. L. Parnas, "Defining the meaning of tabular mathematical
+% expressions," Science of Computer Programming, Vol. 75, no. 11, pp. 980-1000, 2010.
 % * Parnas, D.L., "Tabular Representation of Relations", CRL Report 260,
 % McMaster University, Communications Research Laboratory, TRIO
 % (Telecommunications Research Institute of Ontario), October 1992, 17 pgs.
-% * R. Janicki, D. L. Parnas, and J. Zucker, "Tabular representations in
-% relational documents," in in Relational Methods in Computer Science, pp. 184-196, Springer Verlag, 1996.
+% * R. Janicki, D.L. Parnas, and J. Zucker, "Tabular representations in
+% relational documents," in in Relational Methods in Computer Science, pp. 184-196, Springer Verlag, 1996.
 %% Tabular Expressions in Industry
 % Tabular Expressions have been used in numerous industrial projects, below
 % are some papers describing some of such projects.
 %
-% * A. Wassyng and M. Lawford, "Lessons learned from a successful
-% implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K. Araki, S. Gnesi, and D. Mandrioli, eds.), vol. 2805 of Lecture Notes in Computer Science, pp. 133-153, Springer-Verlag, Aug. 2003.
-% * R. L. Baber, D. L. Parnas, S. A. Vilkomir, P. Harrison, and
-% T. O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp. 428-437, IEEE Computer Society, 2005.
\ No newline at end of file
+% * A. Wassyng and M. Lawford, "Lessons learned from a successful
+% implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K. Araki, S. Gnesi, and D. Mandrioli, eds.), vol. 2805 of Lecture Notes in Computer Science, pp. 133-153, Springer-Verlag, Aug. 2003.
+% * R. L. Baber, D. L. Parnas, S. A. Vilkomir, P. Harrison, and
+% T. O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp. 428-437, IEEE Computer Society, 2005.

html/TT_gs_req.m

@@ -2,12 +2,27 @@
 %
 %% Matlab/Simulink
 %
-% * Tested with Matlab Simulink 2009b and 2010a
+% * Tested with Matlab Simulink 2011b, 2011a, 2010a, 2009b
+%
+%% Table Checking
+% * The tool supports checking of table completness and disjointness
+%  through the support of external tools
+% * This tool will work with either or both of the tools installed.
+% * It is recommened that both tools be installed, as they are built on
+% different technologies, and have different strengths and weaknesses.
+%
+%% CVC3
+% * CVC3 is supported for checking for completness and disjointness of
+% tables
+% * CVC3 can be downloaded from http://cs.nyu.edu/acsys/cvc3/
+% * Ensure that cvc3 is executable on the shell path.
+% * CVC3 is available for Linux/OS X and Windows.
+%
 %% PVS (Prototype Verification System)
-% * PVS is required to be installed in order to check for completness and
+% * PVS is supported for checking for completness and
 % disjointness of tables.
 % * PVS is downloadable from http://pvs.csl.sri.com/
-% * System has been tested on PVS versions 4.2 and 4.1
+% * System has been tested on PVS versions 5.0, 4.2 and 4.1
 % * Ensure that pvs executable is on shell path
-% * *Note:* PVS is a linux and OS X application and will not run natively
-% on Windows.
\ No newline at end of file
+% * *Note:* PVS is a Linux and MacOS X application and will not run natively
+% on Windows.

html/TT_help.m

-%% Table Toolbox
+%% Tabular Expression Toolbox
 %
 % *Available Documentation*
 %
 % * <TT_gs_top.html Getting Started>
+% * <TT_ug.html User Guide>
 %
 % Copyright 2010 Colin Eles

html/TT_ug.m

 %% User Guide
 %
 % * <TT_ug_opening.html Creating a new Table>
-% * <TT_ug_editing.html Editing a Tabular Expression>
+% * <TT_ug_editing.html Editing a Table>
+% * <TT_ug_checking.html Typechecking a Table>
+% * <TT_ug_floating.html Floating Point Numbers>
+% * <TT_ug_saving.html Saving a Table>
 %
 % Copyright 2010 Colin Eles
\ No newline at end of file

html/TT_ug_background.m

+%% Tabular Expressions 
+%
+% 
+

html/TT_ug_checking.m

+%% Typechecking a Table
+%% Overview
+%
+% Of of the main features of tabular expressions is the facilitation of the
+% inspection of completeness and disjointness conditions. This tool has
+% support for external tools to automate this process. Currently two
+% tools based on different ideas and technologies are supported.
+% In order to typecheck a table at least one of these tools must be
+% installed on the system, see the <TT_gs_req.html System Requirements> in the <TT_gs_top.html Getting
+% Started Guide>.
+%
+% It is recommended that both systems be installed as they have different
+% advantages and disadvantages, additionally with both installed a single
+% point of failure for typechecking the table is avoided.
+%
+% The default typechecker is CVC3 as it is easier to install and available
+% for more platforms. however this can be changed from the typecheck
+% menu, see screenshot below.
+%
+% <<ug_check_1.png>>
+%
+% Both tools will appear to operate the same way to the user; the details of how the tools run and
+% their interfaces are hidden from the user of the table tool. If a table
+% is valid the user will be notified with a message box as seen below. if
+% the table is not valid a typechecking report will be generated see below
+% for more details.
+%
+% <<ug_check_3.png>>
+%
+%% Syntax Check
+%
+% Pressing the "Syntax" button or selecting "Syntax Check" from the
+% Typecheck menu will perform a syntactic check on the table. The syntactic
+% check will look at the inputs, conditions, and outputs to ensure that all
+% variables are defined and all expressions are proper Matlab syntax. The syntax check will
+% highlight the problem cells in red as seen in the example below.
+% Condition cells must evaluate to a value that can be interpreted as a
+% boolean value.
+%
+% <<ug_check_10.png>>
+% 
+% In this example the reason there is a syntax error is because the
+% variable declared in the inputs field is x1 whereas the variable being
+% used in the conditions is x. To fix this error one could either change
+% the inputs field to be x or the each x in the table to be x1.
+%
+%% CVC3
+% CVC3 is the third iteration of a SMT solver developed at NYU.
+%
+% *CVC3 Typecheck*
+% 
+% Typecheck the current table using CVC3, will perform a syntax check
+%   prior to running the typecheck operation.
+%
+% *Generate CVC File*
+%
+% Generate a CVC file with the required proof obligations. Calling the typecheck
+% function will also do this, but this function will not attempt to prove
+% the file.
+%
+%% PVS
+% PVS is a general purpose theorem prover developed by SRI. 
+% 
+% *PVS Typecehck*
+%
+% Typecheck the current table using PVS, will perform a syntax check
+%   prior to running the typecheck operation.
+%
+% *PVS Settings*
+%
+% A few settings for running the pvs commands can be adjusted using the pvs
+% settings window. See the screenshot below.
+%
+% <<ug_check_2.png>>
+%
+% * *Imports:* Allows to specify one or more pvs files to import, can be
+% used if other functions or types are referenced.
+% * *Test Count:* Used to adjust the number of attempts when generating a counterexample
+% to an unproven theorem. Increasing this will increase the chances of
+% finding a counterexample but will also increase the time taken to find a
+% counterexample.
+% * *Test Range:* Used to adjust the range of possible counterexamples
+% tested. the range of numbers to test will be in the range (-size..size). 
+% for example if your theorem is only false for the value 500 then you
+% would require a range value >= 500 in order to find the counterexample.
+%
+% *PVS Check Status*
+%
+% Check if the current file has already been typechecked, used when a
+% table was manually proven in pvs rather than being
+% automatically proven using the tool. If the tool fails to generate a
+% counterexample it is possible that the theorem is true but the automatic
+% PVS proof strategies were not sufficient to prove the table, in this case it may be
+% neccessary to prove the table manually using the pvs interface. This
+% command allows you to read the state of the proof into the table tool.
+%
+% *PVS Generate File*
+%
+% Generate a pvs file representing the table. Calling the typecheck
+% function will also do this, but this function will not attempt to prove
+% the file.
+%
+% *PVS Typecheck SimTypes*
+%
+% Typechecking the table with regards to the Simulink types will ignore any
+% typing information in the inputs or function name fields. typng
+% information will be taken from the simulink diagram, so any port
+% datatypes specified in the ports and data manager window will be used.
+% inorder to determine any inherited types the tool will compile the
+% simulink diagram. Therefore any errors in the diagram (alegbraic loops,
+% etc.) will need to be resolved before being able to use this mode of
+% typechecking.
+%
+%% PVS or CVC3
+% PVS and CVC3 are based on 2 different technologies, which means that they
+% will have different advantages and disadvantages. 
+%
+% CVC3 will generally be much faster than PVS, and is usually better at finding a counterexample,
+% however it is not as robust as PVS and if any expressions involve
+% nonlinear mathematics the tool may not perform as expected. As CVC3 is an
+% SMT solver, proving something is an all or nothing operation either the
+% query is valid, invalid, or unknown; there is no way to manually guide or
+% direct the proof in anyway. 
+%
+% PVS is a very general purpose theorem prover, it is very powerful, and as
+% such has a larger overhead than CVC3, as a result it takes longer to run
+% a proof on PVS. PVS's tactics for generating counterexamples is not very
+% sophisticated so it is not always the case that it will find one; it 
+% generally takes a substantial amount of time to run a check for
+% counterexamples. PVS has a robust proof engine that allows for users to
+% manually guide a proof through its completion. When typechecking a table
+% using PVS, PVS may not be able to prove the theorems correct, if a
+% counterexample is not found it may mean that the default proof strategy
+% was not sufficient rather than it being false. In this case the tool allows you to go into pvs to
+% attempt to manually prove the table, this will require knowledge of the
+% pvs proof engine and language, we recomend you find more information here
+% <http://pvs.csl.sri.com http://pvs.csl.sri.com>
+%
+% For these reasons, to get the full power the tool it is recomended that
+% both PVS and CVC3 be installed. Typechecking with both tools eliminates
+% a single point of failure in the typechecking step, and provides greater
+% assurance to the designer that the table is correct.
+%
+%% Typechecking Report
+%
+% If a table fails to be proven valid a typechecking report will be
+% generated. The report serves a number of functions it shows the user what
+% the unproven sequent (logical statement) was, the report will display a counter
+% example should one be generated. The report will highlight in the
+% table the state of cells for the generated
+% counterexamples, this makes it very easy to see where the error was made.
+%
+% Below is the report for a CVC3 typecheck then for a PVS typecheck.
+%
+% <<ug_check_4.png>>
+%
+% <<ug_check_5.png>>
+%
+% There is a minor difference between the CVC3 and the PVS report. The PVS
+% report has a button called "Open" this will open the current theory in
+% PVS allowing for the user to attempt to prove the theorems.
+%
+% If more than one sequent is unproveable, the "next" button will be
+% enabled, this allows the user to view the other unprovable sequents and
+% possible counterexamples.
+%
+% When viewing a sequent that has a counterexample the report will
+% highlight on the table window the state of the conditions.
+%
+% * A *Red* colour indicates that the given cell has evaulated to *False*
+% for the current counterexample.
+% * A *Green* colour indicates that the given cell has evaulated to *True*
+% for the current counterexample.
+%
+% Ideally you want one and only one green cell in each grid. Some examples follow:
+%
+% *Non-disjoint tables*
+%
+% <<ug_check_7.png>>
+%
+% <<ug_check_8.png>>
+%
+% *Incomplete tables*
+% 
+% <<ug_check_6.png>>
+%
+% <<ug_check_9.png>>
+%
+% 
\ No newline at end of file

html/TT_ug_editing.m

 %% Editing a Tabular Expression
 %
-% The Tabular Expression Dialog allows users to graphically layout a
-% tabular expression, for which conditions and outputs can be filled in
-% using the embedded matlab subset of the Matlab languauge.
+% The Table Tool allows users to graphically layout a
+% tabular expression, for which conditions and outputs can be specified
+% using the embedded Matlab subset of the Matlab language.
 %% Layout
 % The Dialog interface allows for the creation of 1-Dimensional vertical
 % and horizontal tables, as well as 2-Dimensional tables. The tool supports
@@ -23,22 +23,93 @@
 % is changed the corresponding output boxes will update as well.
 %% Inputs
 % The input box labeled "Inputs" allows for the specification of inputs to
-% the table. There is no limit in the number of inputs supported. 
+% the table. There is no limit in the number of inputs supported. Inputs
+% are specified in a comma delimited list. names of inputs must conform to
+% the Matlab syntax conventions.
+%
+% *Typing*
+% 
+% Typing information can be specified for each input declared. This allows
+% for users to declare inputs as dependent types. The format for typing follows that of
+% PVS, some examples:
+%
+% * |x, y, z| - 3 inputs with the default type
+% * |x, y:bool| - 2 inputs, y with specified type, x has the default
+% type.
+% * |x:real, y:real, z:bool| - 2 inputs of type real and one of type bool
+% * |x:real, y:{t:real|t>x}| - 2 inputs of type real, y is dependent on x,
+% and is restricted to those value strictly greater than x
+%
 %% Expression Name
+% the expression name will be the name identifying the block, it will also
+% be the function name for generated Matlab code.
+%
+% *Typing*
+%
+% For single output tables, typing information for the output type of the
+% function can be specified in this textbox. formatting for the typing is
+% the same as that for inputs.
+% 
 %% Conditions
-% Text input for a condition box must be valid embedded matlab code.
-% Expressions in condition boxes will be evaulated with the assumed type of
-% boolean. Since embedded matlab is not typechecked this is a pottential
-% cause of errors. By running pvs on a table, each expression in a
+% Text input for a condition box must be valid embedded Matlab code.
+% Expressions in condition boxes will be evaluated with the assumed type of
+% boolean. Since embedded Matlab is not typechecked this is a potential
+% cause of errors. By running a syntax check on a table, each expression in a
 % condition box will be checked that it is of type boolean.
 %
 % For a table with multiple outputs, the horizontal condition boxes
-% represent different outputs. In the example below, the table has 2
-% different outputs labeled, out1 and out2. The syntax of the output specification
-% is the same as for the inputs; this allows for outputs to have
-% different types.
-%
-% <<ug_layout_3.png>>
+% represent different outputs, more detail about this in the following
+% section.
 %
 %% Outputs
-%
\ No newline at end of file
+% The outputs of the function are specified in the outputs grid. Outputs must be an expression that 
+% will evaluate to a definite value. Each output specified should be the same type, however since
+% Matlab is not strongly typed, almost every possible value will be interpreted as a compatible type. 
+% The tool supports 2 output modes: single output and multiple output.
+%
+% The output mode can be specified from the edit menu as seen in the
+% following figure:
+%
+% <<ug_layout_4.png>>
+%
+% *Single Output*
+%
+% For a single output table, the vertical grid can be used for another
+% dimension of conditions. Each output cell shall be a single expression
+% which will evaluate to the output under the interpreted conditions.
+%
+% *Multiple Output*
+%
+% For a table with multiple outputs, the horizontal condition grid is used
+% to specify the outputs of the table. The same rules for typing apply as noted in the 
+% inputs and expression section of this document.
+%
+% Each cell in the condition grid
+% specifies the name (and type) of an output. See the following figure for
+% an example. Each cell in the output grid specifies an output that
+% corresponds to the output specified in the horizontal grid above it.
+%
+% In the example below 
+% the table has 2
+% different outputs labeled, output1 and output2; the outputs have
+% different types. Multiple outputs facilitates robust function specification.
+%
+% <<ug_layout_5.png>>
+%
+%% Ports
+%
+% The "Ports" button will bring up the ports and data manager window (see
+% next figure.) From here you can specify the datatypes of signals, as well
+% as any other functionality as you would with another Simulink block.
+%
+% <<ug_layout_6.png>>
+%
+%% Edit Mode
+% 
+% The edit button is a toggle button which allows for the user to hide the
+% editing buttons which include the new row, delete row, new subgrid, etc.
+% buttons. Hiding these buttons allows for cleaner looking table with fewer
+% distractions allowing the user to concentrate on the content in the
+% table. see an example below.
+%
+% <<ug_layout_7.png>>
\ No newline at end of file

html/TT_ug_floating.m

+%% Working with floating point numbers
+%
+%% Floating point numbers
+% One of the limitations with computers is the way that we have to
+% represent real numbers. In a theoretical sense the real numbers has
+% infinite range and infinite precision, however when we want to represent
+% these numbers in a machine using the standard numerical representation
+% for a variety of reasons we
+% lose these properties.
+%
+% Matlab and most computers use the IEEE 754 floating point standard. The
+% standard defines the way real numbers can be represented from the bit
+% level including the results of operations, and exceptions.
+%
+% A full discussion of the standard is beyond the scope of this document we
+% refer the interested reader to <http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html Matlab's documentation> as well as the
+% <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&tag=1
+% standard documentation>
+%
+%% Proving tables with floating point numbers
+%
+% The toolbox has support for proving tables with floating point inputs.
+% Currently only PVS is supported for this feature, and in general manual
+% intervention with the prover will likely be required.
+%
+% Several new types are provided which can be used as anyother type in the input and output fields.
+% 
+% 
+% * single - a finite or infinite single precision number
+% * single_finite - a finite single precision number
+% * double - a finite or infinite double precision number
+% * double_finite - a finite double precision number
+%
+% A sample input string might be "x:double_finite, y:double_finite". The
+% same rules for subtyping still apply, as it may be necessary to subtype
+% inputs in order to get them to typecheck properly.
+%
\ No newline at end of file

html/TT_ug_opening.m

@@ -11,7 +11,7 @@
 %% Simulink
 %
 % To create a table block in the Simulink environement, open up the block
-% library. Select the Table Toolbox Library. From the Table Toolbox Library
+% library. Select the Tabular Expression Toolbox Library. From the Table Toolbox Library
 % you should see A block Called Tabular Expression, Drag this block to a
 % new or existing model to add a Tabular Expression. Double Click on the
 % block in the model to bring up the Tabular Expression Dialog.
\ No newline at end of file

html/TT_ug_saving.m

+%% Saving a Table
+%
+%% Saving to Block
+%
+% Saving to a block will either save to an existing simulink block or
+% create a new simulink block for the current table. Saving to a block is
+% the default save option so if the "Save" button is pressed it will
+% perform this action.
+%
+% If changes are made in the table interface they will not be updated in the
+% underlying generated code in
+% the simulink block until saving is performed, it is important to remember
+% to save before closing the interface.
+%
+%% Saving to an M-File
+%
+% The Tabular Expression Toolbox allows for users to save their table as an m-function.
+% This allows the function to be called from Matlab scripts or functions;
+% users can also run the function from the command line as a quick way of
+% testing functionality. 
+%
+% To save a table to an m-file select the "save to m-file" command from the
+% file menu as seen in the following screen shot.
+%
+% <<ug_save_1.png>>
+%
+% The toolbox will create a file with the name expression_name.m, where
+% expression_name is the name of your expression. The function can then be
+% called as you would any other function in Matlab, ie.
+% expression_name(arg1,arg2,...)
\ No newline at end of file