%
%
%
%
%
% DON'T USE THIS FUNCTION:  THERE IS A NEW VERSION
%     http://www.cs.toronto.edu/~pedmonds/148/pickup/new-verify.t
%
%
%
%
%
% For CSC148H Summer 96, Assignment 2: Data Encryption
%
%
% VERIFY
% This function will verify that a substitution table is valid.
% It will return true if so, false otherwise.
% The two boolean arrays, verify_plain and verify_cipher, are filled in
% with true for each plaintext letter and ciphertext letter in the
% substitution table.  (Note: the array indices refer to the position in
% the alphabet in the range 1..ALPHA_SIZE of each letter, where ALPHA_SIZE 
% is a constant whose value is the size of the alphabet---26 letters).
% If, after this, either array contains any falses,
% then the substitution table is invalid.  Why?
%
% The only parameter is the substitution table of type subsTableType.
% YOU HAVE TO DEFINE THIS TYPE
%
function verify_table (subs_table : subsTableType) : boolean
    var verify_plain : array 1 .. ALPHA_SIZE of boolean
    var verify_cipher : array 1 .. ALPHA_SIZE of boolean

    % initialize the arrays to all false
    for j : 1 .. ALPHA_SIZE
        verify_plain (j) := false
        verify_cipher (j) := false
    end for

    %%%%%%%%% MAIN LOOP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    % loop through all entries in the substitution table,
    % i refers to the current table entry (which contains a mapping from
    % a single plaintext letter to a ciphertext letter (e.g., "a"->"h"))
    %
    var i : int := 1

    % PRECONDITION  
    assert ( PUT YOUR PRECONDITION(S) HERE )

    % loop through the entries
    loop
        % LOOP INVARIANT
        invariant ( PUT YOUR LOOP INVARIANT HERE )

        exit when (not valid) or (i > ALPHA_SIZE)

        % THE PART IN [] DEPENDS ON YOUR DEFINITION OF THE subsTableType
        var index_plain := [position in alphabet of the plaintext letter
                            in the ith entry of subs_table]
        verify_plain (index_plain) := true

        var index_cipher := [position in alphabet of the ciphertext letter
                             in the ith entry of subs_table]
        verify_cipher (index_cipher) := true

        i := i + 1
    end loop

    % POSTCONDITION
    assert ( PUT YOUR POSTCONDITION(S) HERE )
    
    %
    %%%%%%% end of MAIN LOOP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    % if any entry is still false, then the table is invalid
    for j : 1 .. ALPHA_SIZE
        if (not verify_plain (j) or not verify_cipher (j)) then
            result false
        end if
    end for

    result true
end verify_table