After the notion of variable updating via assignment statements, conditional statements, e.g., as embodied by if <test-expression> then <true-branch-block> else <false-branch-block> structures, are some of the most foundational for programming. Instead of executing statements in a strict sequence, conditional statements let us selectively execute (or avoid executing) blocks of statements based on the current values of program variables as queried by a test expression: if the test-expression evaluates to true then the true-branch-block of statements is executed and the false-branch-block is avoided; if the test-expression evaluates to false then the false-branch-block of statements is executed and the true-branch-block is avoided.

In reasoning about conditional statements, we are often interested in the following questions:

• Under what scenarios is a particular branch executed? For example, when designing a test suite, we typically want to make sure that we have “enough” tests to cause both the true branch and false branch to be executed when running the test suite.

• Is it possible that a particular branch is always (or never) executed? For example, if the false branch can never be executed because the test expression evaluates to true on every possible execution, then the code that we have in the false branch is useful (we commonly refer to the false branch as “dead code”). In this situation, we need to consider if our test expression was improperly code or if it the conditional structure itself should be removed in favor of just providing only the code in the true branch.

• How can we state properties that will be true and the conclusion of a conditional statement, regardless of which branch was executed. Typically we will need such properties to justify the correctness of the complete method/program in which the statement appears.

• What is the “recipe” for tracing facts through a conditional statement as we did for assignment statements?

In this chapter, we first consider a manual process for reasoning about conditional statements, and then we describe Logika’s automated reasoning process for conditionals. Along the way, we introduce various notions related to test design for conditionals.

• Conditionals