Commit d1413759 authored by Colin Eles's avatar Colin Eles
Browse files

latest update, updated help files 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7206 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 0c1c3173

@CVC_checker/cvc_check.m

+3 −3
Original line number Diff line number Diff line
@@ -19,10 +19,10 @@ function [ check, seqs ] = cvc_check( object ) 
[filename, queries] = object.generate_file;



    waitbar(.10,box,'Running Proof');

tic

%tic

    % run the cvc command

[status, result] = system(['cvc3 ' filename ' +model'])

toc

[status, result] = system(['cvc3 ' filename ' +model']);

%toc

% check return status for errors

if (status ~= 0)

@PVS_checker/check_status.m

+1 −1
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ 
% Organization: McMaster Centre for Software Certification

function status = check_status(object)

script_name = object.generate_pvs_status_script(object.data.function_name );

[status, result] = system(['pvs -batch -v 3 -l ' script_name])

[status, result] = system(['pvs -batch -v 3 -l ' script_name]);

parsed = object.parse_status(result);

pass = 1;

if (size(parsed,2) == 0)

@PVS_checker/pvs_check.m

+4 −4
Original line number Diff line number Diff line
@@ -52,7 +52,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) 
    output = 'canceled';

    return;

elseif (exists == 1 && (strcmp(button,'Open PVS')));

    [status, result] = system(['pvs ' function_name '.pvs'])

    [status, result] = system(['pvs ' function_name '.pvs']);

    output = 'canceled';

elseif (exists == 0 || strcmp(button,'Attempt to prove'))

    box = waitbar(0,'Generating Proof Script');
@@ -67,9 +67,9 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) 
    %---------

    % call pvs in batch mode with script

    % ADD check that pvs actually exists in system

    tic

    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])

    toc

    %

    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el']);

    %toc

    %objectect.msgbox_scroll(result);

    waitbar(.70,box,'Parsing Results');

    [parsed error] = object.parse_pvs_result(result);

html/TT_ug.m

+2 −0
Original line number Diff line number Diff line
@@ -3,5 +3,7 @@ 
% * <TT_ug_opening.html Creating a new Table>

% * <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_floating.m

0 → 100644
+37 −0
Original line number Diff line number Diff line 
%% 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