Program Correctness Verification (PCV)

This is a brief description of an upcoming demo to be uploaded and compatible with WebBASIC Reader.

Program Correctness Verification (PCV):

1. Reads and parses TrueBASIC source code;
2. Inserts test directives automatically and without programmer intervention;
3. Executes automatically that test file to trace and map the coverage of code accessibility;
4. Executes in real time the subroutines to determine testability and error;
5. Builds a running product modulo 255 of the resulting 4vbc codes; and
6. Prints the output to screen and file.

(4vbc is "four value bit code" where 00, 01, 10, 11 are the bit values for contradiction, true, false, and tautology; this simple system universally maps deontic, modal, temporal, propositional, and polyadic logics, and recently proved System S5 is not a theorem.)

The result from the error-free demo source code is "10011001" or decimal 153 which is the template for producing the look up table for the EQV operator and which means "conditionally true, conditionally true".

Upcoming are a paper for the DoD software magazine "Cross Talk" and the formal math proof that 4vbc is a vector space. See for applications of 4vbc to philosophy, hardware gates, and software.

PCV may potentially save DoD tens of millions of dollars because it is the first tool mechanically to verify source code as mathematically correct, that is, to verify the requirements of functionality by a mechanical mathematical means. Other versions are in process for Ada2005, C++, FORTH, Fortran, Java, and Python.

Colin James III
CEC Service, LLC
Colorado Springs CO