In order to describe what we understand for Slang programs to be correct, we need some concepts that are best discussed in terms of reasoning about such programs. We begin with very simple Slang program fragments, so that all attention is on the concepts while the program fragments themselves are not of much interest.

The program fragments in this section use

• assignment to immutable variables (val declarations),
• assignment to mutable variables (var declarations),
• sequential composition (represented by writing assigments on consecutive lines).

We begin with the easier discussion on fragments composed immutable variable assignments and then move on to fragments composed of mutable variable assignments. In short,

• Immutable variables are assigned once and then never changed,
• Mutable variables may be assigned multiple times (but at least once).

Although we cannot write very interesting programs using only these constructs, we can make many interesting observations that are essential when handling complicated programs.