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.

!!_begin_loop_setup_number_0001

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

!!_end_loop_setup_number_0001

!!_begin_do_while_not_number_0001

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

!!_begin_do_while_counter_0001

LET index_counter_0001 = index_counter_0001 + index_increment_0001

!!_end_do_while_counter_0001

LOOP

!!_end_do_while_not_number_0001

!!_begin_if_number_0001
IF < another expression > THEN

!!_begin_if_not_number_0001

IF NOT < expression in IF_0001 above > THEN

!!_begin_if_number_0002

IF < yet another expression > THEN
ENDIF

!!_end_if_number_0002

ENDIF

!!_end_if_not_number_0001

ENDIF

!!_end_if_number_0001

Colin James III
CEC Services, LLC
3925 Elisa Ct, Colorado Springs CO 80904
4vbc@cec-services.com
(719) 210 - 9534