There are many ways one can take when designing a language for introducing logics in computer science. Below are the main design criteria for Logika’s:
Based on a real, popular, and modern statically-typed programming language.
This criterion helps with making the case that logics are applicable in real-world settings.
The “statically-typed” part of the criterion is of a personal opinion (i.e., static typing is one showcase of widely-successful applications of logics in computer science, which was introduced to avoid commonly made mistakes; unfortunately, history seems to repeat itself recently) and preference (e.g., it enables various analyses for better IDE support).
Small, yet sufficiently interesting.
Having a large set of well-designed language features are definitely preferable when developing realistic software. However, a small set is desirable in this context to avoid becoming too overwhelming. Yet, the feature set should be sufficiently large to enable case studies on interesting problems. When larger sets are needed, they should be introduced gradually.
Has a “clean” semantic.
“Clean” here really means that the language semantic does not complicate reasoning. For example, 32-bit or 64-bit integers are typically used in most programming languages for efficiency sake. However, they complicate reasoning because one has to worry about underflows/overflows. Such concerns should be separated and considered later once reasoning basics have been grasped. In this particular case, “clean” translates to using arbitrary-precision integers; reasoning to handle ranged or modulo integers can be exposed as additional learning modules.
The above criteria conflict with each other. For example, using arbitrary-precision integers (with arrays indexed by arbitrary-precision index values) often complicates usage and requires a larger set of programming language features (or a library).
The Scala programming language
is chosen as the basis due to its customizability to provide
a clean sandbox for a small, yet interesting language features
(i.e., by leveraging advanced Scala features such as implicits,
macro, and “magic” functions such as apply and update;
see Logika runtime library [github, maven]).
The Logika input formal language are generally categorized into two:
Proof language, for expressing formulae in propositional and predicate logics, as well as for expressing software contracts.
Programming language, for expressing Logika programs.
There are common elements between the two categories (e.g., the expression language). However, they may have some difference, thus, it is convenient to be able to distinguish when the elements are in a certain context by using “proof context” or “programming context”.
The programming language is a simple procedural subset of the
Scala programming language.
The proof language is actually embedded in the programming language,
but they are easily distinguishable because of their reserved form that uses
Scala’s multi-line
string interpolation syntax –
more specifically, l"""{ … }""".
Here is an example to ponder:
import org.sireum.logika._
l"""{ fact
def sum(zs: ZS, n: Z): Z
base. ∀zs: ZS sum(zs, 0) == 0
rec. ∀zs: ZS
∀n: Z
sum(zs, n + 1) == sum(zs, n) + zs(n) }"""
def add(a: ZS): Z = {
l"""{ post result == sum(a, a.size) }"""
var answer: Z = 0
l"""{ 1. answer == 0 premise
2. ∀zs: ZS sum(zs, 0) == 0 fact base
3. sum(a, 0) == 0 ∀e 2 a
4. answer == sum(a, 0) subst2 3 1 }"""
var i: Z = 0
l"""{ 1. answer == sum(a, 0) premise
2. i == 0 premise
3. answer == sum(a, i) subst2 2 1
4. 0 ≤ a.size algebra
5. i ≤ a.size subst2 2 4
6. 0 ≤ i algebra 2 }"""
while (i != a.size) {
l"""{ invariant answer == sum(a, i)
0 ≤ i
i ≤ a.size
modifies answer, i }"""
l"""{ 1. answer == sum(a, i) premise
2. 0 ≤ i premise
3. i ≤ a.size premise
4. i ≠ a.size premise
5. i < a.size algebra 3 4 }"""
answer = answer + a(i)
l"""{ 1. answer == answer_old + a(i) premise
2. answer_old == sum(a, i) premise
3. answer == sum(a, i) + a(i) algebra 2 1
4. ∀zs: ZS
∀n: Z
sum(zs, n + 1) == sum(zs, n) + zs(n) fact rec
5. sum(a, i + 1) == sum(a, i) + a(i) ∀e 4 a i
6. answer == sum(a, i + 1) subst2 5 3
7. i < a.size premise
8. 0 ≤ i premise }"""
i = i + 1
l"""{ 1. answer == sum(a, i_old + 1) premise
2. i == i_old + 1 premise
3. answer == sum(a, i) subst2 2 1
4. 0 ≤ i_old premise
5. 0 ≤ i algebra 2 4
6. i_old < a.size premise
7. i ≤ a.size algebra 2 6 }"""
}
l"""{ 1. answer == sum(a, i) premise
2. not (i ≠ a.size) premise
3. i == a.size algebra 2
4. answer == sum(a, a.size) subst1 3 1 }"""
return answer
}
Let us first discuss the basic language elements that are common to the two categories, before proceeding to discuss the propositional, predicate, and programming logic input languages.