An assertion is the simplest Slang Contract Language construct. 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/constraint 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.

In the Logika symbolic execution engine, for each point in the program, a set of logical constraints on program variables called a “path condition” is generated that represents the properties that must necessarily be true along any execution path that reaches the program point. Then, for each assertion in the program, the Logika engine generates a a verification condition (an obligation to prove during the verification activity) that states that if the path condition for the assertion is true, then the assertion expression is true. Logika sends each verification condition to its underlying SMT solver(s) to prove.
Ideally, the SMT solvers will automatically prove the verification condition (i.e., this is referred to as “discharging” the verification condition). See

for an overview of inner workings of the Logika verification engine.

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

.