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):
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.
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.
stmt : ( 'val' // read-only modifier
| 'var' // read/write 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).
stmt : ( 'val' // read-only modifier
| 'var' // read/write 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.
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.
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.
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).
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).
l"""{
…. P …
…. E … // requires E
}"""
assert(E)
l"""{
…. P premise
…. E premise
}"""
l"""{
…. P …
}"""
assume(E)
l"""{
…. P premise
…. E premise
}"""
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.
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
}"""
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.
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.
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.
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
}"""
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.
l"""{
…. P …
}"""
print (/* … */) // also applies for println
l"""{
…. P premise
}"""
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).
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
}"""
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.
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.
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.
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.
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
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:
Each of them can assume PRE before it starts executing.
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.
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.
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.
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
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:
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.
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 ≤ J ≤ N)
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.
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 ≤ K ≤ M),
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.
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.
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.
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.
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
| 'pbc' sNUM // Proof-by-Contradiction
| '∀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.
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.
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.
just : // …
| 'fact' ID
The fact justification can be used to bring in an axiom
by its identifier in a Proof statement.
l"""{
fact
X. E
}"""
// …
l"""{
Z. E fact X
}"""
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).
l"""{
invariant I
}"""
// …
l"""{
Z. I invariant
}"""
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.
l"""{
X. E1 == E2 …
Y. P{E1}
Z. [E2/E1]P{E1} subst1 X Y
}"""
l"""{
X. E1 == E2 …
Y. P{E2}
Z. [E1/E2]P{E2} subst2 X Y
}"""
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.
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).
l"""{
X1. E1 … // E1 cannot use ∧, ∨, →, ∀, ∃
…
XN. EN … // N > 0, EN cannot use ∧, ∨, →, ∀, ∃
Z. E algebra X1 … XN // if ¬(E1 ∧ … ∧ EN → E) is unsat
}"""
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.
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.
l"""{
X1. E1 …
…
XN. EN … // N > 0
Z. E auto X1 … XN // if ¬(E1 ∧ … ∧ EN → E) is unsat
}"""
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
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).
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
| 'var' // read/write 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
| 'pbc' sNUM // Proof-by-Contradiction
| '∀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
| 'algebra' rNUM*
| 'auto' rNUM*