Slang includes Scala assert statements that can be used to state properties that should hold at the point of the assertion. The argument to an assertion is an arbitrary boolean expression that captures the property of interest:

   var a: Z = 10;   // do some computation
   a = a * 3;

   assert(a == 30); // state a constraint that should hold at this point
   val b: Z = 6;

   assert(a - b < 30 && a - b > 20 && a + b > 30)
                    // the argument to the assertion is an arbitrary
 		   // expression of type B

   assert(a + b > 40)  // results in an assertion violation since
                       // a + b == 36

Assertions play a role in both program execution and verification. During execution, the assertion expression is executed. If the assertion “fails” (i.e., yields an F value), execution is halted and a stack trace (based on the underlying JVM execution of Scala) is printed to the console. For example, when executing the code block above, the assertion assert(a + b > 40) above fails and the following stack trace is generated (excerpts shown):

  java.lang.AssertionError: assertion failed
	at scala.Predef$.assert(Predef.scala:208)
	at Main$$anon$1.<init>(chapter-01.sc:79)
	at Main$.main(chapter-01.sc:1)
	at Main.main(chapter-01.sc)

	...
	
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)

If the assertion succeeds (i.e., yields a T value), then no output is generated and execution continues.

In Slang verification activities, the developer uses the Logika verification framework to prove that there is no program execution that can cause an assertion to fail, i.e., the properties of interest represented by the assertions hold for all executions of the code.

Typically, assertions are used with other Slang specification constructs such as method contracts, invariants, etc. to precisely specify software requirements and/or other key properties that ensure that program execution never results in a run-time exception (e.g., due to bounds violations). Other Slang specification constructs are discussed in ToDo, From John: Give reference