3.1. Basic Language Elements¶

3.1.1. Identifiers¶

Variable and function (method) identifiers are of the following regular expression form: [a-zA-Z][a-zA-Z0-9_]*, i.e., a letter followed by zero of more letters, digits, or underscores. A valid identifier should not be the same as any of Logika operators, literals, and keywords.

Identifiers containing an underscore cannot be used in the programming context (i.e., underscore cannot be a part of a user-declared variable/function identifier).

3.1.2. Operators and Literals¶

Below are a table of Logika operators and literals in both programming and proof context, listed with a decreasing precedence order (first is highest) along with Math Unicode LIVE Shortcuts. Note that the proof context operators and literals include the ones in the programming context, NUM is either 0 or [1-9][0-9]*, STRING is Java’s string literal without the octal escape. The prepend (+:) and implication operators (->, implies, →) are right-associative.

3.1.3. Keywords¶

Logika keywords consists of Scala’s keywords, contract keywords, justification keywords, and type keywords.

abstract       case           catch          class          def
do             else           extends        false          final
finally        for            forSome        if             implicit
import         lazy           macro          match          new
null           object         override       package        private
protected      return         sealed         super          this
throw          trait          try            true           type
val            var            while          with           yield

B              Z              ZS

readInt        randomInt      print          println

pre            requires       modifies       post           ensures
fact           invariant      assert         assume

premise        andi           ande1          ande2          ori1
Vi1            ori2           Vi2            ore            Ve
impliesi       impliese       noti           negi           note
nege           bottome        falsee         pbc
foralli        alli           Ai             foralle        alle
Ae             existsi        somei          Ei             existse
somee          Ee
subst1         subst2         algebra        auto

3.1.4. Comments¶

Logika comments are C99 line (// … until end of the line) and block (/* … */) comments.

Note that block comments are not allowed to appear inside Logika statements (l""" … """).

3.1.5. Newlines and Whitespaces¶

Scala is a line-oriented language where newline characters are treated specially in some cases. For example, newline characters can separate expressions in a code block. The actual rules of when newlines are treated specially are not immediately obvious but they behave “intuitively” (resulting in rare surprises when programming).

Logika follows Scala’s line-orientation (otherwise, it is not a subset language), even inside proof context (e.g., proof steps have to be separated by newlines). For clarity sake, instead of explicitly listing newlines in the Logika context-free grammars that go beyond Scala’s, special situations are described in the relevant sections. Interested readers are referred to the full Logika’s ANTLR4 grammar (NL token) if such details are preferred. (A separate lexical analysis is done after the ANTLR4-generated lexer tokenize an input text to implement Scala’s newline rules, thus, it is not directly specified in the ANTLR4 grammar.)

Other than the special newline rules that Logika follows in proof context, Logika whitespaces are similar to Scala’s.

3.1.6. Grammatical Rules¶

Logika grammars are written in this document using the ANTLR4-style of Backus-Naur Form (BNF) grammar.