RFC for Program Correctness Verifier

This is a Request for Comment (RFC) about group project implementation of the Program Correctness Verifier (PCV) to show the mathematical suitability of source code In TrueBASIC®.

This inquiry is to test the field for interest in an open source project on this subject.

James [see 4-VL.com] shows that the two major procedural software programming constructions are loops and flow control. Loops map to the DO-WHILE-(NOT)-LOOP. Flow control maps to nested IF-(NOT)-THEN-ENDIF. (Other constructs such as SELECT-CASE and WHEN-EXCEPTION-IN are subsets of IF-THEN.)

4VBC is a four-valued logic and calculus that maps programming constructs into truth tables to prove correctness of the structures.

Some details of a proposed convention for embedding directives of PCV into TrueBASIC source code are below.


LET index_begin_0001 =
LET index_end_0001 =
LET index_increment_0001 =
LET increment_sign_0001 = SGN( index_increment_0001)
LET index_counter_0001 = index_begin_0001



DO WHILE NOT ( ( index_end_0001 – index_counter_0001) * increment_sign_0001) >= 0)


LET index_counter_0001 = index_counter_0001 + index_increment_0001




IF < another expression > THEN


IF NOT < expression in IF_0001 above > THEN


IF < yet another expression > THEN






Colin James III
CEC Services, LLC
3925 Elisa Ct, Colorado Springs CO 80904
(719) 210 - 9534