@Grid/upgrade.m

+%% upgrade
+%    Preforms any necessary upgrades to the TET to comply with the latest version.
+% inputs:
+%   object - Grid object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function upgrade( object )
+
+for i=1:size(object.cells, 2)
+    object.cells(i).upgrade
+end
+
+end
+

@PVS_checker/PVS_checker.m

@@ -19,23 +19,23 @@ classdef PVS_checker < handle
     % Static Functions
     methods(Static)
         
-        [theory_id, decls] = parse_prf_file(string)
+        [theory_id, decls] = parse_prf_file(string);
         
         
-        [decl_id,new_pos] = parse_decl_id(string,pos)
+        [decl_id,new_pos] = parse_decl_id(string,pos);
         
         
-        [id,new_pos] = parse_id(string,pos)
+        [id,new_pos] = parse_id(string,pos);
         
         
-        [paren_string, new_pos] = parse_paren(string,pos)
+        [paren_string, new_pos] = parse_paren(string,pos);
         
-        matlab_type = matlab_type_to_pvs_type( pvs_type )
+        matlab_type = matlab_type_to_pvs_type( pvs_type );
         
         
-        version = get_pvs_version
+        version = get_pvs_version;
         
-        [ replaced ] = replace_types_sim( pvs_type, sim_type )
+        [ replaced ] = replace_types_sim( pvs_type, sim_type );
 
         
     end

@PVS_checker/check_status.m

@@ -10,7 +10,7 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function status = check_status(object)
-script_name = object.generate_pvs_status_script(object.data.function_name);
+script_name = object.generate_pvs_status_script(object.data.function_name );
 [status, result] = system(['pvs -batch -v 3 -l ' script_name]);
 parsed = object.parse_status(result);
 pass = 1;
@@ -24,7 +24,7 @@ for i=1:2:size(parsed,2)-1
 end
 
 status = pass;
-delete(script_name);
+delete(script_name)
 
 end
 

@PVS_checker/generate_pvs_file.m

@@ -87,7 +87,17 @@ fileid = fopen([filename '.pvs'],'w');
 code = [];
 code = sprintf('%s:THEORY\nBEGIN\n',function_name);
 %code = [code sprintf('IMPORTING Funcs\n')];
-code = [code object.pvs_check_for_imports];
+imports = object.pvs_check_for_imports;
+if ~isempty(imports)
+    
+    if ~isempty(regexp(imports,'double|single', 'once'))
+        % flag to copy files
+        error = 2;
+    end
+end
+code = [code imports];
+
+
 
 code = [code object.user_imports];
 if object.type_mode
@@ -130,23 +140,7 @@ end
     end
     code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];
     
-%else
-    %inputs_new = [];
-    %for i=1:size(object.input_type,1)
-        
-        
-    %    inputs_new = [inputs_new char(object.input_type(i,1)) ':' PVS_checker.matlab_type_to_pvs_type(char(object.input_type(i,2)))];
-        
-    %    if(i~=(size(object.input_type,1)))
-    %            inputs_new = [inputs_new ','];
-    %    end
-    %end
-    %code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];
-    
-    %code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];
-    
-    
-%end
+
 code = [code object.generate_pvs(object.data.Grid1,object.data.Grid2,0)];
 code = [code sprintf('\nEND %s',function_name)];
 fprintf(fileid,code);

@PVS_checker/generate_pvs_multi_output.m

@@ -37,7 +37,7 @@ for i=1:size(g1.cells,2)
     resultcell = object.data.Grid0.search_return(g1.cells(i),g2_cell);
     if(~isempty(resultcell))
         %if (i == 1)
-        code = [code sprintf('%s',strtrim(char(resultcell.result_text)))];
+        code = [code sprintf('%s',object.matlab_to_pvs_syntax_translation(strtrim(char(resultcell.result_text))))];
         %else
         %    code2 = [code2 sprintf(',%s',strtrim(char(resultcell.result_text)))];
         %end

@PVS_checker/generate_pvs_script.m

@@ -9,10 +9,13 @@
 %    none
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
-function [] = generate_pvs_script(object,filename)
+function [] = generate_pvs_script(object,filename,sim_types)
 fileid = fopen([filename '.el'],'w');
-code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
-
+%if sim_types == 0 
+code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
+%else
+%    code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
+%end
 fprintf(fileid,code);
 fclose(fileid);
 end

@PVS_checker/generate_pvs_status_script.m

@@ -11,7 +11,7 @@
 function [script_name] = generate_pvs_status_script(object,filename)
 script_name = [filename '_status' '.el'];
 fileid = fopen(script_name,'w');
-code = ['(status-proof-pvs-file "' filename '")'];
+code = ['(typecheck-prove "' filename '") (status-proof-pvs-file "' filename '")'];
 
 fprintf(fileid,code);
 fclose(fileid);

@PVS_checker/matlab_to_pvs_syntax_translation.m

@@ -12,12 +12,19 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function pvs_string = matlab_to_pvs_syntax_translation(object,matlab_string)
+s = [matlab_string(1,:)];
+for j = 2:size(matlab_string,1)
+   s = [s ' ' matlab_string(j,:)];
+end
+matlab_string = s;
+
 pvs_string = regexprep(matlab_string,'&&',' AND ');
 pvs_string = regexprep(pvs_string,'~(?!=)',' NOT ');
 pvs_string = regexprep(pvs_string,'~=',' /= ');
 pvs_string = regexprep(pvs_string,'==',' = ');
 pvs_string = regexprep(pvs_string,'\|\|',' OR ');
 pvs_string = regexprep(pvs_string,'ceil','ceiling');
+pvs_string = regexprep(pvs_string,'NaN','invalid');
 end
 
 

@PVS_checker/parse_pvs_result.m

@@ -5,8 +5,8 @@
 %   object:PVS_checker - PVS_checker object
 %   result:string - string containing text that comes back from pvs
 % outputs:
-%   output:structure - results paresed into structure for easier
-%       manipulatings
+%   output:structure - results parsed into structure for easier
+%       manipulating
 %   error:boolean - 0 if no error, 1 if error found during parsing.
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
@@ -24,14 +24,16 @@ else
             % These parsing depend on the version of PVS used,
             % which may be a bad idea, although pvs is not
             
-            if strncmp(object.pvs_version,'PVS Version 4.0',15)
+            if object.pvs_version <= 4.0
                 % find the TCC that was unprovable
                 search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));
-            elseif strncmp(object.pvs_version,'PVS Version 4.2',15)
-                search_str =  sprintf('(?<=Installing rewrite rule singleton_rew\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
+            elseif object.pvs_version <= 4.2
+                search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
+            elseif object.pvs_version >= 5.0
+                search_str =  sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
             end
             found2 = regexp(result,char(search_str),'match','once');
-            
+          
             
             % find the counter examples
             search_str = sprintf('(?<=%s.*?substitutions:).*?(?=This will undo the proof to: \\n%s)|(?<=%s.*?)No counter-examples(?=.*?%s)',char(found(i)),char(found(i)),char(found(i)),char(found(i)));

@PVS_checker/pvs_check.m

@@ -16,12 +16,24 @@ output = [];
 
 function_names = EMLGenerator.parse_inputs(object.data.function_name);
 function_name = char(function_names{1}(1));
+
+
+
+
 error = object.generate_pvs_file(function_name);
 if error == 1
     return;
+elseif error == 2
+    % copy pvs files over.
+    copyfile(fullfile(fileparts(which('TTdiag')),'PVS_theories','*.pvs'),pwd);
+    copyfile(fullfile(fileparts(which('TTdiag')),'PVS_theories','*.prf'),pwd);
 end
 
-object.pvs_version = PVS_checker.get_pvs_version;
+
+
+version_string = PVS_checker.get_pvs_version;
+version = regexp(version_string, 'PVS Version (...)', 'tokens');
+object.pvs_version = str2double(char(version{1}));
 
 
 % THIS SECTION NEEDS SOME WORK
@@ -52,12 +64,14 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     
     
     % generate the proof script
-    object.generate_pvs_script(function_name);
+    object.generate_pvs_script(function_name,1);
     waitbar(.10,box,'Running Proof');
     %---------
     % call pvs in batch mode with script
     % ADD check that pvs actually exists in system
-    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])
+    %
+    [status, result] = safe_execute_external_command(['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);
@@ -76,7 +90,7 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     end
     waitbar(.100,box,'Deleting Proof Script');
     
-    delete([function_name '.el']);
+    %delete([function_name '.el']);
     
     delete(box);
 end

@PVS_checker/pvs_check_for_imports.m

@@ -10,8 +10,73 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function string = pvs_check_for_imports(object)
+
+
+
 [string,found] = object.pvs_check_for_imports_g(object.data.Grid2,{});
 [string2,found2] = object.pvs_check_for_imports_g(object.data.Grid1,found);
+
+
+
+
+
+% check for imports in the inputs field
+
+
+
+hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'} {'double', 'double'} {'single' 'single'}} ;
+
+% check for imports in the results grid.
+for i=1:size(object.data.Grid0.Cells,2)
+
+    text = char(object.data.Grid0.Cells(i).result_text);
+    
+    vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match');
+    
+    
+    
+    
+    for j=1:size(vars,2)
+        if(exist(vars{j},'file')==2 && ~strcmp(vars{j},'otherwise'))
+            %check if already imported file
+            if (~any(ismember(found,vars{j})))
+                string = [string 'IMPORTING ' vars{j} sprintf('\n')];
+                found = [found vars{j}];
+            end
+        end
+        
+        for k=1:size(hashtable,2)
+            if strcmp(vars{j},hashtable{k}(1))
+                if (~any(ismember(found,vars{j})))
+                string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];
+                found = [found vars{j}];
+                end
+            end    
+        end
+    end
+end
+
+
+
+for k=1:size(hashtable,2)
+
+    string_parts = char(object.data.function_inputs);
+    
+    s = [string_parts(1,:)];
+    for j = 2:size(string_parts,1)
+       s = [s ' ' string_parts(j,:)];
+    end
+    string_parts = s;
+    
+    functions = regexp(string_parts,hashtable{k}(1),'once');
+            if ~isempty(functions{1})
+                if (~any(ismember(found,hashtable{k}(1))))
+                string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];
+                found = [found hashtable{k}(1)];
+                end
+            end    
+        end
+        
 string = [string string2];
 end
 

@PVS_checker/pvs_check_for_imports_g.m

@@ -14,15 +14,29 @@
 % Organization: McMaster Centre for Software Certification
 function [string,found] = pvs_check_for_imports_g(object,grid,found)
 string = [];
+
+hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}};
+
 for i=1:size(grid.cells,2)
     % recurse through
     if (~isempty(grid.cells(i).subgrid))
         string = [string object.pvs_check_for_imports_g(grid.cells(i).subgrid)];
     end
     text = char(grid.cells(i).cond_text);
+
+    if size(text) > 0
+        s = [text(1,:)];
+        for j = 2:size(text,1)
+           s = [s ' ' text(j,:)];
+        end
+        text = s;
+    end
     
     vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match');
     
+    
+    
+    
     for j=1:size(vars,2)
         if(exist(vars{j},'file')==2 && ~strcmp(vars{j},'otherwise'))
             %check if already imported file
@@ -31,6 +45,15 @@ for i=1:size(grid.cells,2)
                 found = [found vars{j}];
             end
         end
+        
+        for k=1:size(hashtable,2)
+            if strcmp(vars{j},hashtable{k}(1))
+                if (~any(ismember(found,vars{j})))
+                string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];
+                found = [found vars{j}];
+                end
+            end    
+        end
     end
 end
 end

@RCell/purge.m

+%% purge
+%    Removes useless data from the block on saving, avoiding unnecessary
+%    changes and data storage.
+% inputs:
+%   object - RCell object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function  purge( object )
+object.result = [];
+end
+

@RCell/upgrade.m

+%% upgrade
+%    Preforms any necessary upgrades to the TET to comply with the latest version.
+% inputs:
+%   object - RCell object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function  upgrade( object )
+    if iscell(object.result_text)
+        object.result_text = object.result_text{1};
+    end
+end
+

@RGrid/delete_g1s.m

@@ -17,7 +17,7 @@ for i=1:size(object.Cells,2)
     end
 end
 if(~isempty(deleted))
-    delete(object.Cells(deleted).result);
+    delete([object.Cells(deleted).result]);
     object.Cells(deleted) = [];
 end
 end

@RGrid/delete_g2s.m

@@ -20,7 +20,7 @@ for i=1:size(object.Cells,2)
     end
 end
 if(~isempty(deleted))
-    delete(object.Cells(deleted).result);
+    delete([object.Cells(deleted).result]);
     object.Cells(deleted) = [];
 end
 end

@RGrid/purge.m

+%% purge
+%    Removes useless data from the block on saving, avoiding unnecessary
+%    changes and data storage.
+% inputs:
+%   object - RGrid object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function purge( object )
+for i = 1:size(object.Cells, 2)
+    object.Cells(i).purge;
+end
+
+end
+

@RGrid/upgrade.m

+%% upgrade
+%    Preforms any necessary upgrades to the TET to comply with the latest version.
+% inputs:
+%   object - RGrid object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function upgrade( object )
+for i = 1:size(object.Cells, 2)
+    object.Cells(i).upgrade;
+end
+end
+

@Settings/Settings.m → @TTSettings/TTSettings.m

 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
-classdef Settings < handle
+classdef TTSettings < handle
     %UNTITLED Summary of this class goes here
     %   Detailed explanation goes here
     
@@ -9,6 +9,7 @@ classdef Settings < handle
         pvs_includes = [];
         counter_trials = [];
         counter_range = [];
+        except = [];
         
         % gui elements
         fig_width = 400;
@@ -23,9 +24,10 @@ classdef Settings < handle
         label_width = 75;
         text_offset = 10;
         
-        include_text = []
-        count_text = []
-        range_text = []
+        include_text = [];
+        count_text = [];
+        range_text = [];
+        except_check = [];
     end
     
     methods
@@ -36,7 +38,7 @@ classdef Settings < handle
         %   none
         % outputs:
         %   object:Settings - created object
-        function object = Settings()
+        function object = TTSettings()
         end