Variable Declarations with var and val

Slang uses Scala’s var and val constructs for variable declarations.

• val x - declares x, bound to a given value, and x cannot be reassigned.
• var y - declares y, bound to a given value, and x can be reassigned (giving x a 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 in 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. val 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 val 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. Each declared 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 chapters).

Command Sequencing

Command sequencing / command separation in Slang is indicated using the semicolon ; 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.