Sireum Logika Documentation — 3. The Logika Formal Input Language
3.4. Programming Logic

# 3.4. Programming Logic¶

Logika’s programming logic input language differs from its propositional and predicate logics’ in one main characteristic: variable and function types have to be explicitly specified.

It currently has three built-in types: (1) B – boolean type, (2) Z – arbitrary-precision integer type, and (3) ZS – mutable integer sequence (array) type (whose index and element type is Z with indices starting at 0). There is no null nor top (like Java’s Object or Scala’s Any) values in Logika, which simplify reasonings.

In contrast to regular Scala, Logika’s programming language separates between commands (statements) and queries (expressions). Logika statements are evaluated for their side effect, and expressions are evaluated purely for their resulting value (side-effect free – they do not change values stored in variables). (In Scala, commands are simply expressions whose return value is empty tuple (), which is the Unit type value.) These distinctions are also done to simplify reasonings.

The following pattern notation is used to describe a statement’s side-effects (similar to Proof Schematic Pattern, but enclosed in l"""""" to distinguish it from statement blocks):

Statement Claim Transformation Rule Notation
l"""{ // precondition
…. P                                   …
}"""
statement
l"""{ // postcondition
…. R                                   premise
}"""


P represents any claim that holds (is true) before the statement (precondition) and R represents any claim that holds after the statement (postcondition). The notation uses an identifier such as P and R to represent multiple claims.

In essence, a statement is a claim transformer – a function that transforms its precondition to its postcondition. To relate to program execution, the precondition essentially characterizes the program state before the statement is executed, and the postcondition characterizes the program state after the statement is executed. Thus, the whole program execution can be characterized by composing the claim transformations done by each of the program statements.

As a convention:

• P, Q, and R are used to represent claims.
• X, Y, Z are used to represent variable identifiers and proof step numbers (the two can be easily distinguished).
• ZS (prefix) is used to represent variable identifiers of type ZS.
• T is used to represent a type.
• F is used to represent a function/method identifier.
• E is used to represent a general expression.
• C is used to represent a command/statement or a sequence of statements.

The above can be numbered, for example, X1, X2, etc. In such case, they typically form a series, and N, M, I, J, and K are used to represent some numbers in the series.

The subsequent sections describe Logika’s renditions of programming logic rules that are described in Circuits that Compute on Numbers: Algebra, Programming Logic for Assignments and Conditionals, Functions and Procedures, and Loops and Loop Invariants.

## 3.4.1. Program¶

program    : ( import                     // separated by newline(s)
programElement*            // separated by newline(s)
)?

import      : 'import' 'org' '.' 'sireum' '.' 'logika' '.' '_'

programElement
: stmt
| invariant
| methodDecl
| fact
| import                       // redundant; to allow concatenation of program files into one file


A Logika program can be empty, or it consists of an import statement followed by a zero or more program elements. A program element can be either a Statement, an Invariant, a Method Declaration, or a Fact (axiom or proof function).

Similar to Java or Scala, methods can be forward-referenced (referenced before their declaration). In addition, axioms and proof functions defined in Fact can also be forward-referenced.

## 3.4.2. Statement¶

stmt        : ( 'val'                      // read-only modifier
) ID ':' type '=' rhs        // variable declaration
| ID '=' rhs                   // variable assignment
| 'assert' '(' exp ')'         // assertion
| 'assume' '(' exp ')'         // assumption
| conditional
| whileLoop
| ID '(' exp ')' '=' exp       // sequence element assignment
| print
| 'l"""' '{' proof '}' '"""'   // proof
| 'l"""' '{' sequent '}' '"""' // sequent (auto mode only)
| invoke                       // method invocation


A Logika statement can be either a Variable Declaration and Assignment, an Assertion and Assumption, an If-Else Conditional, a While-Loop, a Sequence Element Assignment, a Print statement, a Proof, or a Sequent (invoke is discussed in Method Invocation).

### 3.4.2.1. Variable Declaration and Assignment¶

stmt        : ( 'val'                      // read-only modifier
) ID ':' type '=' rhs        // variable declaration
| ID '=' rhs                   // variable assignment

type        : 'B'                          // boolean type
| 'Z'                          // integer type
| 'ZS'                         // integer sequence type

rhs         : exp                          // expression
| ID '.' 'clone'               // sequence cloning
| 'randomInt' '(' ')'          // returns a random integer
| 'readInt' '(' STRING? ')'    // reads an integer from console input, STRING is an optional prompt message
| invoke                       // method invocation

invoke      : ID '(' expList? ')'

expList     : exp ( ',' exp )*


A variable declaration is a special assignment form that also declares the variable that it assigns at the same time. The variable has to be declared as either read-only (using the val keyword) – which cannot be reassigned later on, or read/write (using the var keyword). Note that, unlike methods, variables cannot be forward-referenced.

The claim transformation rule for a variable declaration is the same as for assignment. Below are the claim transformation rules for an assignment based on the form of its right-hand side (rhs). Note that any claim referring to the generated _old variable is transient; it does not survive the next (non-proof/sequent) statement. Thus, such claim has to be transformed in a Proof/Sequent statement in order for the information that it contains to be propagated.

Variable Assignment Rule
l"""{
…. P                                   …
}"""
X = E
l"""{
…. [X_old/X]P                          premise
…. X == [X_old/X]E                     premise
}"""


The Variable Assignment Rule indicates that any claim in its precondition is rewritten by substituting the assigned variable X with the newly introduced variable X_old that stores the value of X before the assignment, and the value of X is now equal to the value of expression E where any occurence of X in E is replaced with X_old (which leverages the fact that any Logika expression is pure – side-effect free).

To avoid aliasing issues of mutable objects that complicate reasoning, Logika forces ZS to be cloned (resulting in a new object copy of the sequence) when assigned to a different variable. That is, X = Y are ill-formed if X and Y are of type ZS. It has to be X == Y.clone instead. The ZS cloning rule is as follows.

ZS Cloning Rule
l"""{
…. P                                   …
}"""
X = Y.clone
l"""{
…. [X_old/Y]P                          premise
…. X == Y                              premise
}"""


ZS variable can also be assigned as a result of ZS appending operation (E ≡ E1 :+ E2, where E1 is of type ZS and E2 is of type Z) or prepending operation (E ≡ E1 +: E2, where E1 is of type Z and E2 is of type ZS), both of which also produce a new ZS object (see Expression).

The readInt built-in function asks for an integer input through the program console input (an optional string literal prompt STRING can be provided to display a custom message). Since the resulting integer value depends on the user input, which cannot be predicted, there is no claim that can be stated regarding the value that can be deduced, which is reflected below.

l"""{
…. P                                   …
}"""
X = readInt()  // also applies when a STRING prompt message is provided
l"""{
…. [X_old/Y]P                          premise
}"""


The randomInt built-in function generates a random integer value. Similar to readInt, there is no claim that can be stated regarding the resulting value.

randomInt Rule
l"""{
…. P                                   …
}"""
X = randomInt()
l"""{
…. [X_old/Y]P                          premise
}"""


The rule for invoke is discussed in Method Invocation (substitute occurrence of F_result in the rules with the assigned variable identifier X).

### 3.4.2.2. Assertion and Assumption¶

stmt        : // …
| 'assert' '(' exp ')'         // assertion
| 'assume' '(' exp ')'         // assumption


In Scala, both assertion and assumption methods check whether the specified boolean expression is true; if not, it throws an AssertionError (if assertion checking is enabled).

The two differ in the intention behind them, which are geared for verification purposes. Assertion’s expression has to be proven (i.e., E is required as a precondition of Assertion Rule), while assumption’s expression can be taken as an axiom (i.e., E is not required as a precondition of Assumption Rule, but can be concluded in the postcondition). When a program has been verified, all assertions can be safely erased (to be safe, assumptions should still be runtime checked).

Assertion Rule
l"""{
…. P                                   …
…. E                                   …                 // requires E
}"""
assert(E)
l"""{
…. P                                   premise
…. E                                   premise
}"""

Assumption Rule
l"""{
…. P                                   …
}"""
assume(E)
l"""{
…. P                                   premise
…. E                                   premise
}"""


### 3.4.2.3. If-Else Conditional¶

stmt        : // …
| conditional

conditional : 'if' '(' exp ')' '{'         // conditional
stmt*                      // separated by newline(s)
'}' ( 'else' '{'
stmt*                      // separated by newline(s)
'}' )?


Statements in both Logika if-else conditional branches have to be contained in a code block {}. A conditional can be without the else/false-branch, in which case it is treated as an empty statement block.

The If-Else Conditional Rule specifies that its precondition P holds in the beginning of both branches. In the beginning of the true-branch, the conditional test expression E can be deduced, while its negation ¬E can be deduced in the beginning of the false-branch. At the end of the conditional, the claim R1 ∨ R2 can be deduced, where R1 is the postcondition of C1 and R2 is the postcondition of C2 (if there no such C2, then R2 represents P and ¬E). If R1 ≡ R2, then one can also deduce just R1.

If-Else Conditional Rule
l"""{
…. P                                   …
}"""
if (E) {
l"""{
…. P                                 premise
…. E                                 premise
}"""
C1
l"""{
…. R1                                …
}"""
} else {
l"""{
…. P                                 premise
…. ¬E                                premise
}"""
C2
l"""{
…. R2                                …
}"""
}
l"""{
…. R                                   premise           // R ≡ R1,       if R1 ≡ R2
// R ≡ R1 ∨ R2,  otherwise
}"""


### 3.4.2.4. While-Loop¶

stmt        : // …
| whileLoop

whileLoop   : 'while' '(' exp ')' '{'      // while-loop
loopInvariant?             // separated by newline(s)
stmt*                      // separated by newline(s)
'}'

loopInvariant
: 'l"""' '{'
( 'invariant'
claim*                 // separated by newline(s)
)?
modifies?                  // note: either invariant or modifies has to be present
'}' '"""'

modifies    : 'modifies' idList

idList      : ID ( ',' ID )*


While-loops in Logika can include a loop invariant and a modifies clause (verified programs most likely would include loop invariants and modifies clauses).

The loop invariant specifies the condition that has to be true before (hence, at the beginning of the loop body) and after the statement. At the end of the loop body, the invariant has to be proven to be true. These are reflected in While-Loop Rule.

The invariant can be specified as a sequence of boolean claim expressions; they implicitly form a conjunction where each claim is a conjunct. The main benefit of separating the invariant into several expressions is that Logika can specifically pinpoint which invariant conjunct has yet to be proven as one works through the verification process. In the case that no loop invariant is specified, then it is considered as ⊤.

The modifies clause should comprehensively lists all variables that may be modified by the loop body. The program is ill-formed if the loop body modifies a variable, but it is not listed in the modifies clause. The set of variables that are modified include variables that are assigned in the loop, modified by nested loops, and side-effects of method invocations.

A loop precondition P is also treated as an invariant if it does not refer to any of the variables listed in the loop’s modifies clause. The loop test condition E holds at the beginning of the loop body, and its negation ¬E is a postcondition of loop.

While-Loop Rule
l"""{
…. P
…. I
}"""
while (E) {
l"""{
invariant I
modifies  X1, …, XN
}"""

l"""{
…. P                                 premise           // if P does not refer to X1, …, or XN
…. I                                 premise
…. E                                 premise
}"""
C
l"""{
…. I                                 …
}"""
}
l"""{
…. P                                   premise           // if P does not refer to X1, …, or XN
…. I                                   premise
…. ¬E                                  premise
}"""


When Auto Mode is enabled, auto is implicitly used to satisfy loop invariants whenever possible.

### 3.4.2.5. Sequence Element Assignment¶

stmt        : // …
| ID '(' exp ')' '=' exp       // sequence element assignment


A ZS sequence value stored in a variable X can be mutated by updating one of its elements at a certain index expressed by E1 with a new value expressed by an expression E2 (i.e., X(E1) = E2; see Sequence Element Assignment Rule).

The avoid runtime errors, E1 has to be within the bound of X’s indices, i.e., 0 ≤ E1 and E1 < X.size; thus, they are required as the statement’s precondition. When Auto Mode is enabled, auto is implicitly used to satisfy the precondition whenever possible.

At the postcondition, E1 and E2 and all precondition claims are rewritten to refer to X_old if they refer to X. Similar to the variable assignment rules, any claim referring to the generated _old variable is transient.

The update does not change the size of X, thus, one can deduce X.size == X_old.size. Furthermore, only the updated element got changed to the new value.

Sequence Element Assignment Rule
l"""{
…. P                                   …
…. 0 ≤ E1                              …                 // required to avoid runtime error
…. E1 < X.size                         …                 // required to avoid runtime error
}"""
X(E1) = E2
l"""{
…. [X_old/X]P                          premise
…. X.size == X_old.size                premise
…. X([X_old/X]E1) == [X_old/X]E2       premise
…. ∀q_i: (0 ..< X.size)
q_i ≠ [X_old/X]E1 →
X(q_i) == X_old(q_i)            premise
}"""


### 3.4.2.6. Print¶

stmt        : // …
| print

print       : ( 'print'                    // print without a newline appended
| 'println'                  // print with a newline appended
) '(' printArgList? ')'

printArgList: ( STRING | exp ) ( ',' ( STRING | exp ) )*


The print and println built-in methods are provided for logging purposes (albeit primitive ones). They accept any number of arguments, which can be string literals, and B, Z, and ZS values.

Logika does not reason about their side-effects as they are tangential to Logika’s functional verification focus.

For example, a Logika verified program may still be unsafe if the program console output is piped through a disk and as it turns out, the disk does not have enough space for the printed text. (Similarly, Logika does not guarantee that a program cannot be out of memory.)

At any rate, the two methods do not change program states from Logika’s functional verification perspective, thus, any claim in the precondition can be deduced in the postcondition.

### 3.4.2.7. Proof¶

stmt        : // …
| 'l"""' '{' proof '}' '"""'   // proof

proof       : '{'
proofStep+                 // separated by newline(s)
'}'

proof       : '{'
proofStep+                 // separated by newline(s)
'}'

proofStep   : regularStep
| subProof

regularStep : rNUM '.' claim just          // rNUM is NUM, distinguished for readability of just arguments later

subProof    : sNUM '.'                     // sNUM is NUM, distinguished for readability of just arguments later
'{'
assumeStep                 // separated by newline(s)
proofStep*                 // separated by newline(s)
'}'


A proof statement contains a natural deduction proof similar to a proof in the Predicate Logic and the Propositional Logic languages. It can be used to deduce new claims from existing/transient claims (e.g., to satisfy the subsequent statement’s precondition).

The behavior of a proof statement differs on whether the Auto Mode is enabled. When enabled, the proof statement adds its deduced claims to existing ones. Otherwise, it replaces existing ones with its deduce claims, which results in a Logika program where all deductions necessary to verify the program are forced to be explicitly written (and proof statements intermingled with non-proof/sequent statements as a consequence).

Note that the deduced claims of a proof statement only consists of all claims in regular proof steps at the proof-level (i.e., claims in sub-proofs are excluded).

### 3.4.2.8. Sequent¶

stmt        : // …
| 'l"""' '{' sequent '}' '"""' // sequent (auto mode only)

sequent     : claimList?                   // premises
'⊢'                          // turnstile ("turn-the-style"), can also use '|-' for '⊢'
claimList                    // conclusions

| claim*                       // premises
HLINE                        // HLINE is three or more dashes '-'
claim+                       // conclusions

claimList   : claim ( ',' claim )*


A sequent statement is also similar to the one in the Predicate Logic and Propositional Logic languages. However, it has a different purpose in Logika’s programming logic. That is, it serves as a convenient syntactic sugar for a Proof statement using auto summonings; thus, it can only be used in Auto Mode.

There are two ways the form can be used: with or without premises.

When the sequent premises are specified to automatically deduce its conclusions, i.e.,:

l"""P1,  …,  PN  ⊢  R1,  …, RM"""


it desugars to the following proof statement:

l"""{
1. P1                              premise
…
N. PN                              premise
(N+1). R1                              auto 1 … N
…
(N+M). RM                              auto 1 … N
}"""


When no premise is specified in the sequent, such as:

l"""⊢  R1,  …, RM"""


it desugars to the following proof statement:

l"""{
1. R1                                  auto
…
M. RM                                  auto
}"""


## 3.4.3. Expression¶

exp         : 'true'                       // true literal, can also use 'T' for 'true'
| 'false'                      // false literal, can also use 'F' for for 'false'
| ID                           // variable reference
| NUM                          // integer literal
| 'Z' '(' STRING ')'           // integer literal
| 'ZS' '(' expList? ')'        // sequence literal
| ID '.' size                  // sequence size
| ID '(' exp ')'               // sequence indexing
| '(' exp ')'                  // parenthesized expression
| ( '-' | '!' ) exp            // negative and negation expressions
| exp ( '*' | '/' | '%' ) exp  // multiplicative expression
| exp ( '+' | '-' | '+:' ) exp // additive expression ( '+:' is sequence prepend and it is right-associative)
| exp ':+' exp                 // sequence append
| exp ( '>' | '>='
| '<' | '<=' ) exp       // integer comparison
| exp ( '==' | '!=' ) exp      // equality expression
| exp '&' exp                  // logical-and (non short-circuit) expression
| exp '|' exp                  // logical-or (non short-circuit) expression

expList     : exp ( ',' exp )*


Logika’s expression in the programming context is a subset of its claim expression language in the proof context in that it does not support math symbols and quantifications.

It supports typical operators on integer values, albeit arbitrary-precision. The integer literal form NUM can only be used for value up to 231 - 1; otherwise the Z(STRING) form (e.g., Z("2147483648"), Z("-2147483649")) has to be used instead. This is because Scala’s integer literal by default is a 32-bit signed integer. Logika detects the erroneous situation when NUM is used for integers that cannot fit into 32-bit. It also detects expressions involving 32-bit integer literal that result in values that do not fit into 32-bit such as 1 + 2147483647 and signal an error; this is because such (static) expressions can be optimized to 32-bit integer values when compiled, but they silently overflows/underflows.

Moreover, Logika rejects == and != where the left-hand side is a 32-bit static expression, and the right hand side is not. For example, 5 == x and 5 != x are not allowed; instead, they have to be written as x == 5 and x != 5, respectively. (This is due to Scala’s == and != that accept any type value, which prevents implicit type conversion to Z.) In proof context, one can use the alternative forms of == (=) and != (≠) such as 5 = x and 5 ≠ x. Note that 32-bit static expressions on both sides are allowed such as 5 != 0.

The ZS() literal form is used to create a ZS object whose elements are listed as arguments. For example ZS(2, 5, 3) creates a ZS object whose size is 3 and the element 2 at index 0, 5 at index 1, and 3 at index 2. The ZS append (:+) and prepend (+:) operations create a new ZS object from an existing one.

Unlike a sequence element update, :+ and +: are directly represented in the proof context. For example,

X = Y :+ 2


generates a postcondition claim X == Y :+ 2 instead of:

X.size == Y.size + 1
X(Y.size) == 2
∀q_i: (0 ..< Y.size)  X(q_i) == Y(q_i)


The first two claims can be “extracted” using algebra from X == Y :+ 2, but the last claim can only be extracted using auto (see Algebra (algebra) and Auto (auto)).

Another example,

X = 1 +: X


generates a postcondition claim X == 1 +: X_old, which holds the knowledge:

X.size == X_old.size + 1
X(0) == 1
∀q_i: (1 ..< X.size)  X(q_i) == X_old(q_i - 1)


The direct representations mean fully reasoning about :+ and +: can only be done by enabling Auto Mode. This is done by design instead of due to the Logika’s limitation; at some point, it is best to switch to a more automatic/machine-assisted approach in order not overwhelm oneself with mundane details (and save one’s braincells for solving more interesting problems).

One last thing to note is that & and | operators are logical-and and logical-or operators instead of the short-circuit && and || operators used in many languages such as Java. This is a simplification because short-circuit operators are conditionals; && and || may be added in the future.

The rest of the operations have the typical meaning used in other programming languages.

### 3.4.3.1. Runtime Checks¶

Some operators such as / and % are not defined on certain argument values (i.e., when the divisor is zero). Such situations are typically checked at runtime (e.g., in Java, the VM throws an ArithmeticException for a division by zero).

Instead, Logika requires precondition claims to avoid runtime exceptions/errors when certain expressions are used in the programming context.

Below are the list of expressions that require some precondition related to runtime checks:

• E1 / E2 requires E2 ≠ 0.
• E1 % E2 requires E2 ≠ 0.
• X(E) requires 0 ≤ E and E < X.size.

When Auto Mode is enabled, auto is implicitly used to satisfy the above preconditions whenever possible.

## 3.4.4. Invariant¶

invariant   : 'l"""' '{' 'invariant'
claim+                     // separated by newline(s)
'}' '"""'


The invariant statement declares global invariants that the program’s (non-helper) methods have to maintain. Similar to a loop invariant, the invariant claim expression conjuncts can be specified separately.

The claim expressions have to be proven true before the invariant statements (i.e., precondition of the statement). When Auto Mode is enabled, auto is implicitly used to satisfy all the invariant claims whenever possible.

When Satisfiability Checking Mode is enabled, Logika checks the satisfiability of global invariants to ensure that the program’s specification is useful and implementable.

## 3.4.5. Method Declaration¶

methodDecl  : ( '@' 'helper' )?
'def' ID '(' paramList? ')' ':' ( type | 'Unit' ) '=' '{'
methodContract?
stmt*
( 'return' exp? )?
'}'

methodContract
: 'l"""' '{'
precondition?              // separated by newline(s)
modifies?                  // separated by newline(s)
postcondition?             // separated by newline(s)
'}' '"""'

precondition: 'requires'                   // can also use 'pre' for 'requires'
claim+                     // separated by newline(s)

modifies    : 'modifies' idList

idList      : ID ( ',' ID )*

postcondition
: 'ensures'                    // can also use 'post' for 'ensures'
claim+                     // separated by newline(s)


A Logika method can have an associated contract that specifies its precondition (claims that have to be true in order for the method to properly function), modifies clause (that comprehensively lists all variables that will be modified by the method, similar to the modifies clause in the modifies clause in loop invariants), and postcondition (claims that the method has to satisfy once it finishes executing). If the precondition or the postcondition are not specified, then they are treated as ⊤. Moreover, if the modifies clause is not specified, that means the method does not modify any variable (pure).

Note that Logika method parameter variables cannot be assigned (read-only); but, any parameter variable of type ZS can have its element assigned as ZS is a mutable sequence. A method whose return type is Unit is considered as not returning a value; otherwise, the resulting value is captured in a special variable named result, which can be referred to in the method’s postcondition.

In general, there are two kinds of methods in Logika: helper and regular (non-helper) methods; helper methods are declared by using the @helper annotation, and regular ones are those without the annotation. Regular methods maintain the program global Invariant, while helper methods do not have to.

That is, a regular method: (1) can assume the program global invariant when it starts to execute, (2) do not have to maintain the invariant during its execution, and (3) have to re-establish the invariant by the end of its execution (only for invariant claims that refer to modified global variables as the other claims are not affected); these are reflected in Method Declaration Rule. In essence, the invariant claims are both precondition claims and postcondition claims of regular methods; effective precondition and effective postcondition are used to refer to precondition and postcondition that include global Invariant claims, respectively.

Method Declaration Rule
l"""{
invariant I                                              // I can be represented by multiple claims
}"""
// …
def F(/* … */) ':' /* … */ = {
l"""{
requires  PRE                                          // precondition
modifies  X1, …, XN                                    // modifies clause
ensures   POST                                         // postcondition
}"""

l"""{
…. I                                 premise           // (1) can assume I
…. PRE                               premise           // (A) can assume PRE
…. X1 == X1_in                       premise           // (B) for any modified variable XI, XI == XI_in
…
…. XN == XN_in                       premise           // (B)
}"""
C                                                        // (2) statements C do not need to maintain I during its execution
l"""{
…. I                                 …                 // (3) have to re-establish I (only claims referring to X1, …, XN)
…. [E/result]POST                    …                 // (C) have establish POST
}"""
( return E? )?
}


On the other hand, helper methods: (1) cannot assume the program global invariant when it starts to execute, (2) do not have to maintain the invariant during its execution, and (3) do not have to establish the invariant by the end of its execution; these are reflected in Helper Method Declaration Rule.

Helper Method Declaration Rule
@helper
def F(/* … */) ':' /* … */ = {
l"""{
requires  PRE                                          // precondition
modifies  X1, …, XN                                    // modifies clause
ensures   POST                                         // postcondition
}"""

l"""{                                                    // (1) cannot assume the program global invariant I
…. PRE                               premise           // (A) can assume PRE
…. X1 == X1_in                       premise           // (B) for any modified variable XI, XI == XI_in
…
…. XN == XN_in                       premise           // (B)
}"""
C                                                        // (2) C do not need to maintain I the during its execution
l"""{                                                    // (3) do not have to establish I
…. [E/result]POST                    …                 // (C) have establish POST
}"""
( return E? )?
}


Helper and regular methods have some similarities. That is:

1. Each of them can assume PRE before it starts executing.
2. For any modified variable XI, it can assume XI == XI_in before it starts executing. The _in variables represent the corresponding variable values before they are modified during the execution, and they can be referred in claim expressions (in proof context) throughout the method’s body and in its postcondition claims.
3. The method has to establish POST. If the method’s return type is not Unit, it has to return a value, expressed by E and stored in the special variable result as previously mentioned. The variable result can be used on POST; hence, at the end of the method [E/result]POST has to be established.

When Auto Mode is enabled, auto is implicitly used to satisfy postcondition (and invariant) whenever possible. Moreover, when Satisfiability Checking Mode is enabled, Logika checks the satisfiability of the method contract.

## 3.4.6. Method Invocation¶

invoke      : ID '(' expList? ')'

expList     : exp ( ',' exp )*


Method invocations for regular and helper methods also differ slightly. First, helper methods can only be invoked from other methods. Invoking a regular method requires the program global invariant, while it is not required when invoking a helper method. After the invocation of a regular method, the global invariant is available because the method ensures it, which is not the case when invoking a helper method. These are reflected in Method Invocation Rule and Helper Method Invocation Rule.

Method Invocation Rule
l"""{
invariant I
}"""
// …
def F(X1: T1, /* … */, XN: TN) ':' /* … */ = {
l"""{
requires  PRE
modifies  Y1, …, YM
ensures   POST
}"""
// …
}

// …
l"""{
…. P                                   …
…. I                                   …                 // global invariant I has to be established since F requires it
…. [EN/YN]…[E1/Y1]PRE                  …
}"""
F(E1, /* …, */ EN)                                         // invoke regular method F with arguments E1, …, EN for parameters X1, …, XN
l"""{
…. I                                   premise           // global invariant I is available since F ensures it
…. P3                                  premise
…. POST3                               premise
// 1. P1        ≡ P
//    POST1     ≡ [F_result/result]POST
// 2. For 1 < I ≤ N,
//      P2-1    ≡ [ZS1_old/ZS1]P, if E1 is a variable ZS1 (of type ZS) and X1 is in {Y1, …, YM}
//              ≡ P, otherwise
//      P2-I    ≡ [ZSI_old/ZSI]P2-(I-1), if EI is a variable ZSI and XI is in {Y1, …, YM}
//              ≡ P2-(I-1), otherwise
//      POST2-1 ≡ [ZS1_old/X1_in][ZS1/X1][ZS1_old/ZS1]POST1, if E1 is a variable ZS1 and X1 is in {Y1, …, YM}
//              ≡ POST1, otherwise
//      POST2-I ≡ [ZSI_old/XI_in][ZSI/XI][ZSI_old/ZSI]POST2-(I-1), if EI is a variable ZSI and XI is in {Y1, …, YM}
//              ≡ POST2-(I-1), otherwise
// 3. P3        ≡ [YM_old/YM_in]…[Y1_old/Y1_in]P2-N
//    POST3     ≡ [YM_old/YM_in]…[Y1_old/Y1_in]POST2-N
}"""

Helper Method Invocation Rule
@helper
def F(X1: T1, /* … */, XN: TN) ':' /* … */ = {
l"""{
requires  PRE
modifies  Y1, …, YM
ensures   POST
}"""
// …
}

// …
l"""{
…. P                                   …
…. [EN/YN]…[E1/Y1]PRE                  …
}"""
F(E1, /* …, */ EN)                                         // invoke helper method F with arguments E1, …, EN for parameters X1, …, XN
l"""{
…. P3                                  premise
…. POST3                               premise
// 1. P1        ≡ P
//    POST1     ≡ [F_result/result]POST
// 2. For 1 < I ≤ N,
//      P2-1    ≡ [ZS1_old/ZS1]P, if E1 is a variable ZS1 (of type ZS) and X1 is in {Y1, …, YM}
//              ≡ P, otherwise
//      P2-I    ≡ [ZSI_old/ZSI]P2-(I-1), if EI is a variable ZSI and XI is in {Y1, …, YM}
//              ≡ P2-(I-1), otherwise
//      POST2-1 ≡ [ZS1_old/X1_in][ZS1/X1][ZS1_old/ZS1]POST1, if E1 is a variable ZS1 and X1 is in {Y1, …, YM}
//              ≡ POST1, otherwise
//      POST2-I ≡ [ZSI_old/XI_in][ZSI/XI][ZSI_old/ZSI]POST2-(I-1), if EI is a variable ZSI and XI is in {Y1, …, YM}
//              ≡ POST2-(I-1), otherwise
// 3. P3        ≡ [YM_old/YM_in]…[Y1_old/Y1_in]P2-N
//    POST3     ≡ [YM_old/YM_in]…[Y1_old/Y1_in]POST2-N
}"""


The result and side-effects of invoking a regular or a helper method F are as follows:

1. Any reference to result in the method’s postcondition is substituted with F_result (POST1 in Method Invocation Rule or Helper Method Invocation Rule). Note that any claim referring to F_result is transient similar to _old variables. As described in Variable Declaration and Assignment, if the result is assigned to a variable X, then F_result is further substituted with X (not shown in Method Invocation Rule or Helper Method Invocation Rule). P cannot refer to result, thus, P1 ≡ P.

2. F might modify ZS values which are passed as parameters. The effects of the modifications can only be observed after the invocation if the arguments for the parameters are variables of type ZS because other expression forms that of type ZS (i.e., ZS(), :+, and +:) produce a new ZS object that cannot be referred after the invocation.

POST2-J and P2-J (for 1 ≤ JN) capture the effects of modifications of ZS values passed as parameters whose arguments are variables. More specifically, for each parameter XJ of type ZS, if XJ is modified and the argument EJ for XJ is a variable ZSJ, then, any occurrence of ZSJ is substituted with ZSJ_old in P2-(J-1) and POST2-(J-1); otherwise P2-J ≡ P2-(J-1) and POST2-J ≡ POST2-(J-1). Additionally, XJ is substituted with ZSJ and XJ_in is substituted with ZSJ_old in POST2-J.

3. F might modify global variables. The effects of the modifications are captured in P3 and POST3. More specifically, for any modified variable YK (for 1 ≤ KM), YK_in is substituted with YK_old in P2-N and POST2-N. Note that YK could actually be a parameter, in which case the substitution is harmless because the parameter has been substituted in the previous step.

## 3.4.7. Fact¶

fact        : 'l"""' '{' 'fact'
( axiom | proofFunction )+ // separated by newline(s)
'}' '"""'

axiom       : ID '.' claim

proofFunction
: 'def' ID '(' paramList ')' ':' type

paramList   : param ( ',' param )*

param       : ID ':' type

type        : 'B'                          // boolean type
| 'Z'                          // integer type
| 'ZS'                         // integer sequence type


A fact statement can be used to introduce global (named) axioms and (pure) proof functions (whose behaviors are specified via axioms) to help with specifying contracts.

While axioms are assumed to hold, Logika can check their satisfiability to ensure their consistency by enabling Satisfiability Checking Mode; an unsatisfiable axiom claim reduces to ⊥, thus, it can render any specification to be proven by using ⊥-Elimination (⊥e).

In Auto Mode, all axioms are implicitly used to help deduce claims in auto summoning without arguments.

## 3.4.8. Extended Assume Step¶

assumeStep  : rNUM '.' claim 'assume'
| rNUM '.' ID ':' type         // ID must be "fresh" in scope; used for ForAll-Introduction
| rNUM '.' ID ':' type
claim 'assume'               // ID must be "fresh"; used for Exists-Elimination


The assume step in programming logic differs slightly than the one in Predicate Logic where fresh variables now have to be explicitly typed.

## 3.4.9. Extended Claim Expression¶

claim       : '⊤'                          // true literal, can also use 'T' or 'true' for '⊤'            (also apply in just)
| '⊥'                          // false literal, can also use 'F', 'false', or '_|_' for '⊥'  (also apply in just)
| ID                           // identifier
| 'result'                     // method result (only in postcondition of methods whose return type is not Unit)
| NUM                          // integer literal
| 'Z' '(' STRING ')'           // integer literal
| 'ZS' '(' claimList? ')'      // sequence literal
| ID '.' size                  // sequence size
| ID '(' claimList? ')'        // predicate application
| '(' claim ')'                // parenthesized claim expression
| '-' claim                    // negative integer claim expression
| '¬' claim                    // negation, can also use 'not', 'neg', ''!', or '~' for '¬'    (also apply in just)
| claim ( '*' | '/' | '%' )
claim                        // multiplicative claim expression
| claim ( '+' | '-' | '+:' )
claim                        // additive claim expression ( '+:' is sequence prepend and it is right-associative)
| claim ':+' claim             // sequence append
| claim ( '>'
| '≥'                  // can also use '>=' for '≥'
| '<'
| '<='                 // can also use '<=' for '≤'
) claim                // integer comparison
| claim ( '==' | '!=' ) claim  // equality claim expression
| claim '∧' claim              // conjunction/and, can also use '&', 'and', or '^' for '∧'     (also apply in just)
| claim '∨' claim              // disjunction/or, can also use '|', 'or', or 'V' for '∨'       (also apply in just)
| claim '→' claim              // implication, can also use '->' or 'implies' for '→'          (also apply in just)
| ( '∀'                        // univ. quant., can also use 'forall', 'all', 'A' for '∀'      (also apply in just)
| '∃'                        // exist. quant., can also use 'exists', 'some', 'E' for '∃'    (also apply in just)
) idList ':' domain claim

domain      : type                         // type domain
| '('                          // integer range type domain
claim '<'?                 // integer low-range bound, exclusive if '<' is specified
'..'
'<'? claim                 // integer high-range bound, exclusive if '<' is specified


The claim expression language is extended from the one in Predicate Logic that adds Z and ZS literals, in/equality tests, and arithmetic and ZS operations, as highlighted above.

In addition to having an explicit type for quantified variables (type domain), Logika allows an integer range domain of the form ( integer low bound .. integer high bound ); by default, the range is inclusive; < can be used to in either side of .. to indicate exclusive range for the low and/or high bounds, respectively.

## 3.4.10. Extended Justification and Inference Rules¶

just        : 'premise'
| '∧i'      rNUM rNUM          // And-Introduction
| '∧e1'     rNUM               // And-Elimination1
| '∧e2'     rNUM               // And-Elimination2
| '∨i1'     rNUM               // Or-Introduction1
| '∨i2'     rNUM               // Or-Introduction2
| '∨e'      rNUM sNUM sNUM     // Or-Elimination
| '→i'      sNUM               // Implication-Introduction
| '→e'      rNUM rNUM          // Implication-Elimination
| '¬i'      sNUM               // Negation-Introduction
| '¬e'      rNUM rNUM          // Negation-Elimination
| '⊥e'      rNUM               // ⊥-Elimination
| '∀i'      sNUM               // Forall-Introduction
| '∀e'      rNUM claim+        // Forall-Elimination
| '∃i'      rNUM claim+        // Exists-Introduction
| '∃e'      rNUM sNUM          // Exists-Elimination
| 'fact'    ID
| 'invariant'
| 'subst1'  rNUM rNUM
| 'subst2'  rNUM rNUM


The justification form in Logika’s programming logic extends Propositional Logic’s Or-Elimination (∨e) and Predicate Logic’s Quantified Claim Justification and Inference Rules, as well as adding new ones as highlighted above.

### 3.4.10.1. Or-Elimination (∨e)¶

The Or-Elimination (∨e) Schematic Pattern and Alternative Or-Elimination (∨e) Schematic Pattern are extended to also work for ≤ and ≥, where E1 ≤ E2 is treated as E1 < E2  ∨  E1 == E2, and E1 ≥ E2 is tread as E1 > E2  ∨  E1 == E2.

### 3.4.10.2. Quantified Claim Inference Rules (∀i, ∀e, ∃i, ∃e)¶

Quantifications using the integer range domain form are simplified first before applying Quantified Claim Justification and Inference Rules.

For example, the claim ∀x: (0 ..< 3)  P{x} is simplified first to ∀x: Z  0 ≤ x ∧ x < 3 → P{x} before applying any of the ∀-quantified claim rules.

Another example, the claim ∃x: (0 ..< 3)  P{x} is simplified first to ∃x: Z  (0 ≤ x ∧ x < 3) ∧ P{x} before applying any of the ∃-quantified claim rules.

### 3.4.10.3. Fact (fact)¶

just        : // …
| 'fact'    ID


The fact justification can be used to bring in an axiom by its identifier in a Proof statement.

Fact Schematic Pattern
l"""{
fact
X. E
}"""
// …
l"""{
Z. E                                   fact X
}"""


### 3.4.10.4. Invariant (invariant)¶

just        : // …
| 'invariant'


Similar to the fact justification, invariant can be used to bring in an invariant claim. Since invariant claims are unnamed, the justification does not require an argument (unlike fact). Note that invariant can only be used in a Proof statement that is outside of a method (top-level).

Invariant Schematic Pattern
l"""{
invariant I
}"""
// …
l"""{
Z. I                                   invariant
}"""


### 3.4.10.5. Substitutions (subst1 and subst2)¶

just        : // …
| 'subst1'  rNUM rNUM
| 'subst2'  rNUM rNUM


The two substitution justifications can be used to substitute claim expressions E1 and E2 that are equal to each other (E1 == E2); subst1 substitutes E1 with E2, while subst2 substitutes E2 with E1.

Substitution1 (subst1) Schematic Pattern
l"""{
X. E1 == E2                            …
Y. P{E1}
Z. [E2/E1]P{E1}                        subst1 X Y
}"""

Substitution2 (subst1) Schematic Pattern
l"""{
X. E1 == E2                            …
Y. P{E2}
Z. [E1/E2]P{E2}                        subst2 X Y
}"""


## 3.4.11. Summonings¶

just        : // …
| 'algebra' rNUM*
| 'auto'    rNUM*


Logika summonings are special justifications. Up until now, all deduction justifications are directly checked by Logika. Summoning justifications are distinguished because the deductions are checked by leveraging the work of giants, such as by employing Z3’s powerful automatic satisfiability checking (the reader might be interested to see a classical example and/or a modern example on how summoning works).

Currently, there are two summonings in Logika: algebra and auto, both of which use Z3 to check the deductions. Note that although Z3 is quite powerful, Z3 cannot always automatically deduce claims, for example, when they involve non-linear integer arithmetic, which no automated technique can always solve. As a consequence, there are programs that cannot be verified by Logika. Other summonings involving more elaborate incantations will be added in the future to address this.

### 3.4.11.1. Algebra (algebra)¶

just        : // …
| 'algebra' rNUM*


The algebra summoning can be used to automatically deduce algebraic arithmetic claims. It cannot be used to reason about claims that contain a conjunction, a disjunction, an implication, or a quantification. This is by design and it is done to force reasoning about claims involving propositional and predicate logic operators using their respective inference rules.

The algebra summoning can be used with or without arguments; its usages are depicted in Algebra Schematic Pattern (with some arguments) and Algebra Schematic Pattern (without argument).

Algebra Schematic Pattern (with some arguments)
l"""{
X1. E1                                 …                 // E1 cannot use ∧, ∨, →, ∀, ∃
…
XN. EN                                 …                 // N > 0, EN cannot use ∧, ∨, →, ∀, ∃
Z.  E                                  algebra X1 … XN   // if ¬(E1 ∧ … ∧ EN → E) is unsat
}"""

Algebra Schematic Pattern (without argument)
l"""{
Z.  E                                  algebra           // if ¬E is unsat
}"""


The algebra summoning is available regardless of whether the Auto Mode is enabled; however, it is subsumed by the auto summoning, which is described next.

### 3.4.11.2. Auto (auto)¶

just        : // …
| 'auto'    rNUM*


The auto summoning can only be used in Auto Mode. It is similar to algebra, but without its restrictions. That is, it can be used to reason about any claim expression form. Moreover, in contrast to algebra, auto uses all axioms and premises when used without arguments.

Auto Schematic Pattern (with some arguments)
l"""{
X1. E1                                 …
…
XN. EN                                 …                 // N > 0
Z.  E                                  auto X1 … XN      // if ¬(E1 ∧ … ∧ EN → E) is unsat
}"""

Auto Schematic Pattern (without argument)
l"""{
X1. P1                                 …
…
XK. PM                                 …
Z.  E                                  auto              // if ¬(premise1 ∧ … ∧ premiseN ∧ axiom1 ∧ … ∧ axiomM ∧ P1 ∧ … ∧ PM → E) is unsat
}"""                                                       // where:
// * premiseI comes from the postcondition of the preceeding statement
// * axiomI is an axiom declared in a fact


## 3.4.12. Well-formed-ness¶

The well-formed-ness rules for Logika’s programming language are similar to that of statically typed languages such as identifiers cannot be re-declared, expressions cannot refer to undeclared variables, and expressions are well-typed (do not have a type mismatch).

## 3.4.13. Programming Logic Input Language Grammar¶

Note that extended language elements from that of the Predicate Logic Input Language Grammar are highlighted.

program    : ( import                     // separated by newline(s)
programElement*            // separated by newline(s)
)?

import      : 'import' 'org' '.' 'sireum' '.' 'logika' '.' '_'

programElement
: stmt
| invariant
| methodDecl
| fact
| import                       // redundant; to allow concatenation of program files into one file

fact        : 'l"""' '{' 'fact'
( axiom | proofFunction )+ // separated by newline(s)
'}' '"""'

axiom       : ID '.' claim

proofFunction
: 'def' ID '(' paramList ')' ':' type

paramList   : param ( ',' param )*

param       : ID ':' type

type        : 'B'                          // boolean type
| 'Z'                          // integer type
| 'ZS'                         // integer sequence type

invariant   : 'l"""' '{' 'invariant'
claim+                     // separated by newline(s)
'}' '"""'

methodDecl  : ( '@' 'helper' )?
'def' ID '(' paramList? ')' ':' ( type | 'Unit' ) '=' '{'
methodContract?
stmt*
( 'return' exp? )?
'}'

methodContract
: 'l"""' '{'
precondition?              // separated by newline(s)
modifies?                  // separated by newline(s)
postcondition?             // separated by newline(s)
'}' '"""'

precondition: 'requires'                   // can also use 'pre' for 'requires'
claim+                     // separated by newline(s)

modifies    : 'modifies' idList

idList      : ID ( ',' ID )*

postcondition
: 'ensures'                    // can also use 'post' for 'ensures'
claim+                     // separated by newline(s)

stmt        : ( 'val'                      // read-only modifier
) ID ':' type '=' rhs        // variable declaration
| ID '=' rhs                   // variable assignment
| 'assert' '(' exp ')'         // assertion
| 'assume' '(' exp ')'         // assumption
| conditional
| whileLoop
| ID '(' exp ')' '=' exp       // sequence element assignment
| print
| 'l"""' '{' proof '}' '"""'   // proof
| 'l"""' '{' sequent '}' '"""' // sequent (auto mode only)
| invoke                       // method invocation

rhs         : exp                          // expression
| ID '.' 'clone'               // sequence cloning
| 'randomInt' '(' ')'          // returns a random integer
| 'readInt' '(' STRING? ')'    // reads an integer from console input, STRING is an optional prompt message
| invoke                       // method invocation

conditional : 'if' '(' exp ')' '{'         // conditional
stmt*                      // separated by newline(s)
'}' ( 'else' '{'
stmt*                      // separated by newline(s)
'}' )?

whileLoop   : 'while' '(' exp ')' '{'      // while-loop
loopInvariant?             // separated by newline(s)
stmt*                      // separated by newline(s)
'}'

loopInvariant
: 'l"""' '{'
( 'invariant'
claim*                 // separated by newline(s)
)?
modifies?                  // note: either invariant or modifies has to be present
'}' '"""'

invoke      : ID '(' expList? ')'

expList     : exp ( ',' exp )*

print       : ( 'print'                    // print without a newline appended
| 'println'                  // print with a newline appended
) '(' printArgList? ')'

printArgList: ( STRING | exp ) ( ',' ( STRING | exp ) )*

exp         : 'true'                       // true literal, can also use 'T' for 'true'
| 'false'                      // false literal, can also use 'F' for for 'false'
| ID                           // variable reference
| NUM                          // integer literal
| 'Z' '(' STRING ')'           // integer literal
| 'ZS' '(' expList? ')'        // sequence literal
| ID '.' size                  // sequence size
| ID '(' exp ')'               // sequence indexing
| '(' exp ')'                  // parenthesized expression
| ( '-' | '!' ) exp            // negative and negation expressions
| exp ( '*' | '/' | '%' ) exp  // multiplicative expression
| exp ( '+' | '-' | '+:' ) exp // additive expression ( '+:' is sequence prepend and it is right-associative)
| exp ':+' exp                 // sequence append
| exp ( '>' | '>='
| '<' | '<=' ) exp       // integer comparison
| exp ( '==' | '!=' ) exp      // equality expression
| exp '&' exp                  // logical-and (non short-circuit) expression
| exp '|' exp                  // logical-or (non short-circuit) expression

proof       : '{'
proofStep+                 // separated by newline(s)
'}'

proof       : '{'
proofStep+                 // separated by newline(s)
'}'

proofStep   : regularStep
| subProof

regularStep : rNUM '.' claim just          // rNUM is NUM, distinguished for readability of just arguments later

subProof    : sNUM '.'                     // sNUM is NUM, distinguished for readability of just arguments later
'{'
assumeStep                 // separated by newline(s)
proofStep*                 // separated by newline(s)
'}'

sequent     : claimList?                   // premises
'⊢'                          // turnstile ("turn-the-style"), can also use '|-' for '⊢'
claimList                    // conclusions

| claim*                       // premises
HLINE                        // HLINE is three or more dashes '-'
claim+                       // conclusions

claimList   : claim ( ',' claim )*

assumeStep  : rNUM '.' claim 'assume'
| rNUM '.' ID ':' type         // ID must be "fresh" in scope; used for ForAll-Introduction
| rNUM '.' ID ':' type
claim 'assume'               // ID must be "fresh"; used for Exists-Elimination

claim       : '⊤'                          // true literal, can also use 'T' or 'true' for '⊤'            (also apply in just)
| '⊥'                          // false literal, can also use 'F', 'false', or '_|_' for '⊥'  (also apply in just)
| ID                           // identifier
| 'result'                     // method result (only in postcondition of methods whose return type is not Unit)
| NUM                          // integer literal
| 'Z' '(' STRING ')'           // integer literal
| 'ZS' '(' claimList? ')'      // sequence literal
| ID '.' size                  // sequence size
| ID '(' claimList? ')'        // predicate application
| '(' claim ')'                // parenthesized claim expression
| '-' claim                    // negative integer claim expression
| '¬' claim                    // negation, can also use 'not', 'neg', ''!', or '~' for '¬'    (also apply in just)
| claim ( '*' | '/' | '%' )
claim                        // multiplicative claim expression
| claim ( '+' | '-' | '+:' )
claim                        // additive claim expression ( '+:' is sequence prepend and it is right-associative)
| claim ':+' claim             // sequence append
| claim ( '>'
| '≥'                  // can also use '>=' for '≥'
| '<'
| '<='                 // can also use '<=' for '≤'
) claim                // integer comparison
| claim ( '==' | '!=' ) claim  // equality claim expression
| claim '∧' claim              // conjunction/and, can also use '&', 'and', or '^' for '∧'     (also apply in just)
| claim '∨' claim              // disjunction/or, can also use '|', 'or', or 'V' for '∨'       (also apply in just)
| claim '→' claim              // implication, can also use '->' or 'implies' for '→'          (also apply in just)
| ( '∀'                        // univ. quant., can also use 'forall', 'all', 'A' for '∀'      (also apply in just)
| '∃'                        // exist. quant., can also use 'exists', 'some', 'E' for '∃'    (also apply in just)
) idList ':' domain claim

domain      : type                         // type domain
| '('                          // integer range type domain
claim '<'?                 // integer low-range bound, exclusive if '<' is specified
'..'
'<'? claim                 // integer high-range bound, exclusive if '<' is specified
')'

just        : 'premise'
| '∧i'      rNUM rNUM          // And-Introduction
| '∧e1'     rNUM               // And-Elimination1
| '∧e2'     rNUM               // And-Elimination2
| '∨i1'     rNUM               // Or-Introduction1
| '∨i2'     rNUM               // Or-Introduction2
| '∨e'      rNUM sNUM sNUM     // Or-Elimination
| '→i'      sNUM               // Implication-Introduction
| '→e'      rNUM rNUM          // Implication-Elimination
| '¬i'      sNUM               // Negation-Introduction
| '¬e'      rNUM rNUM          // Negation-Elimination
| '⊥e'      rNUM               // ⊥-Elimination