tagged v0.3 of table tool

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

classdef CVC_checker

    %CVC_CHECKER Summary of this class goes here

    %   Detailed explanation goes here

    properties

    methods

        %% CVC_checker

        %    constructor

        % inputs:

        %   data:Data - data to generate from

        % outputs:

        %   object:CVC_checker - generated object.

        function object = CVC_checker(data)

            object.data = data;

        end

%% cvc_check

% checks a table using cvc, parses results and returns them

%

% inputs:

%   object:cvc_checker - cvc_checker object

%

% outputs;

%   check:boolean - 0 if check fails, 1 if succeds

%   seqs:structure - if typecheck succeds then output contains

%       parsed output from cvc

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [ check, seqs ] = cvc_check( object )

%CVC_CHECK Summary of this function goes here

%   Detailed explanation goes here

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

    % run the cvc command

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

% check return status for errors

if (status ~= 0)

    if (status == 127)

seqs = [];

% look for incompleteness, happens with non-linear artihmetic, ie.

% % multiplication

% incomplete = regexp(result,'CVC3 was incomplete in this example due to','match');

% if ~isempty(incomplete)

%     incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once')

%     msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]);

%     

%         check = 0;

%         seqs = 'canceled';

%         delete(box);

%         return;

%     

% end

% look for parse errors

fatal_exception = regexp(result,'*** Fatal exception');

        % formula was found to be invalid

        % look for a counter example

        asserts =  regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match');

%         for j = 1:size(asserts,2)

%             splits = {splits regexp(asserts(j),'=','split')};

% 

%         end

    if mod(i,2) == 1

        name = [filename '_' num2str(i) '_DIS'];

%% find_parents

% function will find all the parents of a cell, used to determine what

% preconditions must be true.

%

% inputs:

%   cell:Cell - cell to find the parents of

%

% outputs;

%   code:string - string of conjunction of all parent cells.

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [ code ] = find_parents( cell )

% assumption, initial input will be grid we want to find parents for not

% parent cell itself

%  cell itself

code = '';

if isempty(cell)

%% genereate_cvc_grid

% generate the queries for cvc for the inputted grid.

%

% inputs:

%   grid:Grid - grid to generate conditions for.

%   level:int - count of the queries generated.

%

% outputs;

%   code:string - string representing code to generate including comments

%   query:cell array - contains string representing both the disjoint and

%   complete without the comments, used for validation report.

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [ code , query] = generate_cvc_grid( grid , level)

%GENERATE_CVC_GRID Summary of this function goes here

%   Detailed explanation goes here

% generate the formulas for the main grid

for i=1:size(grid.cells,2)

%   1

%   2  

%   3

%   

%   1 2

%   1 3

%   2 3

%   

%   1 2 3 4

%   1 2

%   1 3

%   1 4

%   

    for j = i+1:size(grid.cells,2)

        % compare i to j

%% genereate_file

% generate the cvc file to be inputted into cvc, calls the generate grid

% function. generates all the variable declarations.

%

% inputs:

%   object:CVC_checker - current object.

%

% outputs;

%   filename:string - the filename of the generated file

%   queries:cell arrray - a list of queries generated by the grids.

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [ filename, queries ] = generate_file( object )

%GENERATE_FILE Summary of this function goes here

%   Detailed explanation goes here

function_names = EMLGenerator.parse_inputs(object.data.function_name);

function_name = char(function_names{1}(1));

end   

% generate grid 2

char(code);

fileid = fopen([function_name '.cvc'],'w');

fprintf(fileid,'%s',char(code));

fclose(fileid);