Updating revision number and documentation to add NFM2011 reference and website.

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

%

%% Matlab/Simulink

%

% * Tested with Matlab Simulink 2009b and 2010a

% * Tested with Matlab Simulink 2011a, 2010a, 2009b

%

%% Table Checking

% * The tool supports checking of table completness and disjointness

% * PVS is downloadable from http://pvs.csl.sri.com/

% * System has been tested on PVS versions 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

% * *Note:* PVS is a Linux and MacOS X application and will not run natively

% on Windows.

<toc version="2.0">

<!-- First tocitem specifies top level in Help browser Contents pane -->

<!-- This can be a roadmap page, as shown below, or a content page -->

    <tocitem target="html/TT_help.html">MyToolbox Toolbox

    <tocitem target="html/TT_help.html">Tabular Expression Toolbox

        <!-- Nest tocitems to create hierarchical entries in  Contents-->

        <!-- To include icons, use the following syntax for tocitems: -->

        <!-- <tocitem target="foo.html" image="HelpIcon.NAME"> -->

        <!-- matlabroot/toolbox/matlab/icons -->

        <!-- A Getting Started Guide usually comes first -->

        <tocitem target="html/TT_gs_top.html" image="HelpIcon.GETTING_STARTED">

            Getting Started with the MyToolbox Toolbox

            Getting Started with the Tabular Expression Toolbox

            <tocitem target="html/TT_gs_req.html">System Requirements

            </tocitem>

            <tocitem target="html/TT_gs_over.html">Product Overview

        <!-- First item is page describing function categories, if any -->

        <!-- Optional link or links to your or other Web sites -->

        <tocitem target="http://www.mathworks.com" 

        <tocitem target="http://www.cas.mcmaster.ca/~lawford/TET" 

                 image="$toolbox/matlab/icons/webicon.gif">

        MyToolbox Web Site (Example only: goes to mathworks.com)

        Tabular Expression Toolbox Web Site

        </tocitem>

    </tocitem>

<toc version="2.0">

<!-- First tocitem specifies top level in Help browser Contents pane -->

<!-- This can be a roadmap page, as shown below, or a content page -->

    <tocitem target="mytoolbox_product_page.html">MyToolbox Toolbox

    <tocitem target="mytoolbox_product_page.html">Tabular Expression Toolbox

        <!-- Nest tocitems to create hierarchical entries in  Contents-->

        <!-- To include icons, use the following syntax for tocitems: -->

        <!-- <tocitem target="foo.html" image="HelpIcon.NAME"> -->

        <!-- First item is page describing function categories, if any -->

        <!-- Optional link or links to your or other Web sites -->

        <tocitem target="http://www.mathworks.com" 

        <tocitem target="http://www.cas.mcmaster.ca/~lawford/TET" 

                 image="$toolbox/matlab/icons/webicon.gif">

        MyToolbox Web Site (Example only: goes to mathworks.com)

        Tabular Expression Toolbox Web Site

        </tocitem>

    </tocitem>

<html><head>

      <meta http-equiv="Content-Type" content="text/html; charset=utf-8">

   <!--

This HTML is auto-generated from an M-file.

To make changes, update the M-file and republish this document.

      --><title>Product Overview</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-11-25"><meta name="m-file" content="TT_gs_over"><style type="text/css">

This HTML was auto-generated from MATLAB code.

To make changes, update the MATLAB code and republish this document.

      --><title>Product Overview</title><meta name="generator" content="MATLAB 7.12"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2011-08-23"><meta name="DC.source" content="TT_gs_over.m"><style type="text/css">

body {

  background-color: white;

Error in ==> TT_gs_over at 35

if(x>0)

</pre><p>If we go back and look at our model window we can see that our Tabular Expression block has updated based on our specified inputs and outputs.</p><p><img vspace="5" hspace="5" src="walk5.png" alt=""> </p><h2>Proving a Table<a name="6"></a></h2><p>Let us assume that a table designer has specified the following function table:</p><p><img vspace="5" hspace="5" src="walk6.png" alt=""> </p><p>In order for a tabular expression to be considered "proper" it must satisfy a <b>Completness</b> and <b>Disjointness</b> condition</p><div><ul><li>Completness means that in the specification of a function we have considered all possible inputs in a condition cell.</li><li>Disjointness means that in the specification of a function all condition cells in a grid are pairwise disjoint, in other words for all possible inputs it is not the case that two conditions are true at the same time.</li></ul></div><p>We desire these properties to ensure that our function is total and is deterministic. A function that is not total or not deterministic can have undesired effects, potentially causing safety critical problems depending on the requirements of the software. The graphical layout of a table helps the designer to evaluate a table for these conditions. Some times it is a non-trivial problem to determine if these conditions have been meet, so we employ the use of a theorem proving software to mechanically prove the properties.</p><p>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 process dialog as shown below:</p><p><img vspace="5" hspace="5" src="walk7.png" alt=""> </p><p>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.</p><p><img vspace="5" hspace="5" src="walk8_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk8_p2.png" alt=""> </p><p>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. In this senario pvs has found that a counter example to the formula is x = 1. When a counter example is found the tool will give visual feedback on which conditions were true and which were false for that counter example. A condition coloured red indicates that the condition was false for the given counter example, a green colour indicates that a condition is true. For this example we can see that both possible conditions are false for the counter example indicating to the table designer that they failed to consider a case of the input.</p><p><img vspace="5" hspace="5" src="walk9_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk9_p2.png" alt=""> </p><p>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 both cells green to indicate to the user that for the counter example of x = 0 both of these conditions are true, the designer has failed to unambiguosly specify what should happen in this senario.</p><p class="footer"><br>

      Published with MATLAB&reg; 7.10<br></p></div><!--

</pre><p>If we go back and look at our model window we can see that our Tabular Expression block has updated based on our specified inputs and outputs.</p><p><img vspace="5" hspace="5" src="walk5.png" alt=""> </p><h2>Proving a Table<a name="6"></a></h2><p>Let us assume that a table designer has specified the following function table:</p><p><img vspace="5" hspace="5" src="walk6.png" alt=""> </p><p>In order for a tabular expression to be considered "proper" it must satisfy a <b>Completness</b> and <b>Disjointness</b> condition</p><div><ul><li>Completness means that in the specification of a function we have considered all possible inputs in a condition cell.</li><li>Disjointness means that in the specification of a function all condition cells in a grid are pairwise disjoint, in other words for all possible inputs it is not the case that two conditions are true at the same time.</li></ul></div><p>We desire these properties to ensure that our function is total and is deterministic. A function that is not total or not deterministic can have undesired effects, potentially causing safety critical problems depending on the requirements of the software. The graphical layout of a table helps the designer to evaluate a table for these conditions. Some times it is a non-trivial problem to determine if these conditions have been meet, so we employ the use of a theorem proving software to mechanically prove the properties.</p><p>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 Typecheck button will start the proof and popup a process dialog as shown below:</p><p><img vspace="5" hspace="5" src="walk7.png" alt=""> </p><p>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.</p><p><img vspace="5" hspace="5" src="walk8_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk8_p2.png" alt=""> </p><p>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. In this senario pvs has found that a counter example to the formula is x = 1. When a counter example is found the tool will give visual feedback on which conditions were true and which were false for that counter example. A condition coloured red indicates that the condition was false for the given counter example, a green colour indicates that a condition is true. For this example we can see that both possible conditions are false for the counter example indicating to the table designer that they failed to consider a case of the input.</p><p><img vspace="5" hspace="5" src="walk9_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk9_p2.png" alt=""> </p><p>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 both cells green to indicate to the user that for the counter example of x = 0 both of these conditions are true, the designer has failed to unambiguosly specify what should happen in this senario.</p><p class="footer"><br>

      Published with MATLAB&reg; 7.12<br></p></div><!--

##### SOURCE BEGIN #####

%% Product Overview

% This product allows users to interactively design a tabular expression.

%%

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