Variable Declarations with
Slang uses Scala’s
val constructs for variable
val x- declares
x, bound to a given value, and
xcannot be reassigned.
var y- declares
y, bound to a given value, and
xcan be reassigned (giving
xa new value).
var i: Z = 0;
// var x: Z; // error: every val/var must be given an initial value
var j: Z = i + 1; // initializers can be expressions
var k = 1; // variable types can be inferred, but not recommended style
i = i + k; // variables declared with var can be reassigned
val b: B = true;
// b = (i == 0) // error: cannot assign to read-only variable b (declared with 'val')
Each Slang variable must explicitly be given an initial value.
In addition, Scala’s mechanism for indicating a default value is not supported. This follows other high-assurance languages such as SPARK that require explicit initialization before variable use to avoid errors associated with uninitialized variables and to ensure that the programmer/analyst always has the correct understanding of a variable’s initial value. A variable’s initial value can be computed from an expression that references previously declared variables.
A type declaration for variable is optional. Slang’s type inference allows local variables to be declared without a type by inferring it from the initializing expression. However, it is best practice to declare each variable with a type to indicate its intended use and to enable the Slang type checker to detect any unintended mismatches between the intended type of the variable and the type of the initializing expression. Moreover, Slang requires explicit type declaration if the initializing expression is complex (e.g., branching).
Variables declared with
var can be re-assigned, as illustrated by
the update to
i = i + k. Slang uses the symbol
= for assignment, while
== is the equality operator
(following Scala, and other languages like Java and C).
“Variables” declared with
val cannot be reassigned.
declarations are often used as “constants” would be in other
languages (e.g., Java’s
final or C’s
const) and when
supporting a functional programming style for Slang, achieving the
conventional functional programming notion of “identifiers bound to values”.
While it is possible to use
var to declare a variable that is
never updated, explicitly using
val to state the intent that a variable never
changes is a useful specification notion in high-assurance
programming. The use of
val in Slang also has a significant
impact on the way that the declared variable is treated in the Logika
verification infrastructure. For example, since Logika knows that
variables never change, there is no need for the developer
to state an explicit frame
condition on a non-local
val indicating that its value is
the same in the pre-state as well as the post-state of a method.
val on an immutable type introduced above has an implicit
associated “invariant” that constrains its value to always be
its initial value (we will discuss immutable and mutable types in the subsequent
Command sequencing / command separation in Slang is indicated using
; as in many other languages. However,
Slang also supports Scala’s line-orientation so
semicolons can sometimes be omitted:
i = i + k // ';' can be omitted in Slang due to Scala's line-orientation
j = k * 2
Stylistically, choosing to use semicolons or not is a personal
preference, though for readability it is best to use one approach consistently.
When adopting the “line-orientation” style, one should be familiar with Scala’s rules for semicolon inference (give the result) since some of its outcomes may be non-intuitive.