Formal Specifications - Abstract State Machine Model Language (ASML)

COMP201 Lectures 2021-10-20

This lecture covers model based specifications. We use models to specify the behaviour of a system.

Abstract State Machine Language (ASML)

An ASML model is an abstract model that only encodes the aspects of the systems structure that affect the behaviour being modelled.

• The goal is the use the minimum amount of detail that accurately reproduces the behaviour of the system that we which to model.

Abstraction helps us reduce complex problems into manageable units and prevents us from getting lost in implementation details.

Example with Sets

Consider that we have a set that includes integers from one to 20. We want to find the numbers from the set, that when doubled, still belong to the set.

This is the solution in ASML:

A = {1..20}
C = {i|i in A where 2 * i in A}

Main()
	step
		WriteLine(C)

Sequences

Elements of sequences are contained in square brackets:

[1,2,3,4]

They are ordered and can contain duplicate elements.

Sequences Example

The following output is produced when then code is run:

X={1,2,3,4}
Y={1,1,2,3,4}
Z=[1,1,2,3,4]
Main()
	step WriteLine("X=" + X)
	step WriteLine("Y=" + Y)
	step WriteLine("Z=" + Z)

X={1,2,3,4}
Y={1,2,3,4}
Z=[1,1,2,3,4]

Curly braces {} denote sets so they are simplified on assignment.

Bubble Sort in ASML

To complete a bubble sort in ASML you can use the following code:

var A as Seq of Integer

swap()
	choose i in {0..length(A)-1}, j in {0..length(A)-1} where i < j and A(i) > A(j)
		A(j) := A(i)	# these happen as one atomic operation as there is no `step` keyword
		A(i) := A(j)	# as a result this swaps the variables

sort()
	step until fixpoint	# fixpoint is true when no data changes
		swap()

Main()
	step A := [-4, 6, 9, 0, 2, -12, 7, 3, 5, 6]	# test list hard-coded 
	step WriteLine("Sequence A:")
	step sort()
	step WriteLine("after sorting:" + A")

Quick-Sort in ASML

To complete a quick-sort, with left had pivot, in ASML you would use the following code:

qsort(s as Seq of Integer) as Seq of Integer	# takes a Seq of Integer and returns a Seq of Integer
	if s = [] then
		return []	# base case
	else pivot = Head(s)	# recursive step, head as pivot
	rest = Tail (s)
		# return less than pivot, pivot and greater than/equal to pivot
		return qsort([y | y in rest where y < pivot]) + [pivot] + qsort([y | y in rest where y ≥ pivot])
Main() 
   WriteLine(qsort([7, 8, 2, 42]))	# test list hard-coded