From ec9aa6191700a572324e1cdae6231a731d65cfb1 Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Thu, 14 Apr 2011 17:53:32 +0000 Subject: [PATCH] tagged v0.4 release with floating point features git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/tags/TableTool/v0.4@7210 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- @CVC_checker/cvc_check.m | 6 +- @GUI/GUI.m | 2 +- @PVS_checker/check_status.m | 2 +- @PVS_checker/pvs_check.m | 8 +-- @PVS_checker/pvs_check_for_imports.m | 2 +- html/TT_ug.m | 2 + html/TT_ug_floating.m | 37 ++++++++++ html/html/TT_ug.html | 9 +-- html/html/TT_ug_floating.html | 103 +++++++++++++++++++++++++++ 9 files changed, 157 insertions(+), 14 deletions(-) create mode 100644 html/TT_ug_floating.m create mode 100644 html/html/TT_ug_floating.html diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m index 7cc2e10..3cd1360 100644 --- a/@CVC_checker/cvc_check.m +++ b/@CVC_checker/cvc_check.m @@ -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) diff --git a/@GUI/GUI.m b/@GUI/GUI.m index 784d11d..40673ba 100644 --- a/@GUI/GUI.m +++ b/@GUI/GUI.m @@ -64,7 +64,7 @@ classdef GUI < handle multi_opt_out = []; prover_opt_pvs = []; prover_opt_cvc = []; - version = '0.3.1'; + version = '0.4'; undo_man = []; undo_opt = []; redo_opt = []; diff --git a/@PVS_checker/check_status.m b/@PVS_checker/check_status.m index 890ee9c..6093e94 100644 --- a/@PVS_checker/check_status.m +++ b/@PVS_checker/check_status.m @@ -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) diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m index 0833d35..5cad2c4 100644 --- a/@PVS_checker/pvs_check.m +++ b/@PVS_checker/pvs_check.m @@ -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); diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m index 7b4deeb..8f958c3 100644 --- a/@PVS_checker/pvs_check_for_imports.m +++ b/@PVS_checker/pvs_check_for_imports.m @@ -60,7 +60,7 @@ end for k=1:size(hashtable,2) - functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once') + functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once'); if ~isempty(functions{1}) if (~any(ismember(found,hashtable{k}(1)))) string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')]; diff --git a/html/TT_ug.m b/html/TT_ug.m index 00116f0..8c7df3b 100644 --- a/html/TT_ug.m +++ b/html/TT_ug.m @@ -3,5 +3,7 @@ % * % * % * +% * % * +% % Copyright 2010 Colin Eles \ No newline at end of file diff --git a/html/TT_ug_floating.m b/html/TT_ug_floating.m new file mode 100644 index 0000000..d37c4f5 --- /dev/null +++ b/html/TT_ug_floating.m @@ -0,0 +1,37 @@ +%% 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 as well as the +% +% +%% 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 diff --git a/html/html/TT_ug.html b/html/html/TT_ug.html index 30dafd5..e46cfa9 100644 --- a/html/html/TT_ug.html +++ b/html/html/TT_ug.html @@ -6,7 +6,7 @@ User Guide

User Guide

Copyright 2010 Colin Eles


+

User Guide

Copyright 2010 Colin Eles


Published with MATLAB® 7.10

Working with floating point numbers

Working with floating point numbers

Contents

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 Matlab's documentation as well as the 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


+ Published with MATLAB® 7.10

\ No newline at end of file -- GitLab