2015/10/17 by Sander in 't Veld, Veld, Sander in 't
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1510.05162
openalex publication_date 2015/10/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The logical connectives typically found in programming languages are similar to their mathematical counterparts, yet different due to their short-circuit behaviour -- when evaluating them, the second argument is only evaluated if the first argument is not sufficient to determine the result. Combined with the possibility of side-effects, this creates a different type of logic called Short Circuit Logic. A greater theoretical understanding of this logic can lead to more efficient programming and faster program execution. In this thesis, formula satisfiability in the context of Short Circuit Logic is discussed. A formal definition of evaluation based on valuation algebras is presented, alongside an alternative definition based on valuation paths. The accompanying satisfiability and `path-satisfiability' are then proven to be equivalent, and an implementation of path-satisfiability is given. Although five types of valuation algebras can be discerned, there are only three corresponding types of valuation paths. From this, conclusions are drawn about satisfiability and side-effects; the manner in which side-effects alter truth values is relevant when analysing satisfiability, but the side-effects themselves are not.