AsmL/NET

AsmL - the Abstract State Machine Language, and in its .NET incarnation often written AsmL/NET or AsmL for Microsoft .NET - is an executable specification language built by the Foundations of Software Engineering group at Microsoft Research. It is a formal methods language that compiles to CLR assemblies, interoperates with any other .NET code, and was authored, in its flagship configuration, inside a Microsoft Word document.

That last detail is not a curiosity. AsmL was designed to answer a specific complaint about formal specification: that specs are written in a notation nobody on the team reads, checked by nobody, and out of date within a month. AsmL’s answer was that a specification should be a document a program manager can read, containing code a compiler can run and a test generator can explore. Whether that answer worked is the interesting part of AsmL’s history.

History and Origins

The theory came first. Yuri Gurevich spent the late 1980s and early 1990s developing what he called evolving algebras, later renamed abstract state machines. The central claim - stated in the 1993 Lipari Guide and refined afterwards - is a thesis about computation itself: every algorithm can be simulated step-for-step by an abstract state machine operating at the algorithm’s own level of abstraction. No encoding into Turing tapes, no loss of structure. If you can describe what a step of your algorithm does, an ASM can be that description.

The practical consequence is that ASMs are a specification method with no fixed level of abstraction. The same formalism describes a hardware protocol, an operating system component, or a business process, and refinement between those levels is a relation you can state precisely rather than a hand-wave.

In 1998 Microsoft Research invited Gurevich to form a group and apply the method to industrial software. His first hire was Wolfram Schulte, and the Foundations of Software Engineering (FSE) group grew from there - Mike Barnett, Wolfgang Grieskamp, Margus Veanes, Colin Campbell, Lev Nachmanson, Nikolai Tillmann and others. Their early work was case studies: the ASM 2000 paper Using Abstract State Machines at Microsoft modelled the debugger of a stack-based runtime environment, and further work in the group applied the same runtime-checking idea to component implementations, comparing their behaviour against ASM specifications.

Doing this repeatedly made the tooling gap obvious. Existing ASM tools - the ASM Workbench, XASM, AsmGofer and others from the academic community - were fine for research but were not going to be adopted by Microsoft product teams. MSR-TR-2001-98, Toward Industrial Strength Abstract State Machines, is essentially the design document for what came next: extend sequential ASMs with object orientation, structured values and submachine composition, and give them a language that a .NET developer will recognise.

The AsmL project page at Microsoft Research records the project as established on November 2, 2001. The first tutorial is dated December 19, 2001, revised May 23, 2002 for the .NET version. By June 2002 AsmL 1.5 was circulating publicly enough to be covered on Slashdot. AsmL 2 - the .NET generation, the one the surviving manuals document - is what the name AsmL/NET refers to.

Design Philosophy

A specification you can run. This is the whole argument. An AsmL model compiles and executes, so the question does this specification actually do what we intended has an experimental answer. You can explore a design before writing the system, and you can keep running the specification against the implementation afterwards.

One document, three audiences. AsmL shipped with a Microsoft Word add-in supporting literate programming: prose, diagrams and executable AsmL in the same document, with the compiler extracting the code. Program managers, developers and testers were meant to work from the same artefact. In an organisation where the spec was traditionally a Word document that developers stopped reading, this was a deliberate piece of social engineering as much as a technical feature.

Abstraction is the point, not a cost. AsmL provides sets, sequences, maps and tuples as first-class mathematical values with comprehension syntax, so a model can say the set of all pending requests without committing to a data structure. The model is allowed to be inefficient; it is not allowed to be vague.

Non-determinism is expressible. Real specifications underspecify on purpose. choose lets a model say that some element is picked without saying which, and the test generator can then explore the branches rather than being fooled into treating an arbitrary implementation choice as required behaviour.

Live inside .NET, not beside it. AsmL generates .NET assemblies that can be run from the command line, linked against other assemblies, or packaged as COM components. A model can call into production code and production code can call into a model. This is what made conformance testing practical.

Key Features

The step: simultaneous updates

The core semantic idea, and the one that surprises newcomers most. Within a step, all updates are collected into an update set and committed atomically when the step ends. Reads see the old state throughout.

var A as Integer = 1
var B as Integer = 2

Main()
  A := B
  B := A
  step
    WriteLine( "A is " + A + " and B is " + B + "." )

This swaps A and B. No temporary variable, because both right-hand sides are evaluated against the state at the start of the step. The step keyword marks the transition to the next state, so by the time WriteLine runs, the updates have been committed.

The same mechanism gives AsmL its consistency check: if a single step tries to update the same location to two different values, that is an inconsistent update set, and it is an error rather than a race. A specification cannot accidentally depend on the order in which its own parallel assignments happened to run.

Hello, world

Main()
  WriteLine("Hello, world!")

Blocks are delimited by indentation rather than braces - and the tutorial is emphatic that AsmL does not recognise tab characters, so indentation must be spaces. Main() is the top-level entry point by convention, in the same role as main in C, and the language is case-sensitive.

Parallel and sequential composition

forall runs a body for every element of a collection in parallel, collecting all the resulting updates into one step; step foreach runs them in sequence, one step each; choose picks one element non-deterministically.

class Person
  var age as Integer

Main()
  forall p in People
    p.age := p.age + 1        // everybody ages in a single step
  step
    WriteLine("done")

These three constructs - forall, step/while, choose - generalise parallel, sequential and non-deterministic composition respectively, and they are the reason AsmL models read as descriptions of behaviour rather than as programs.

Mathematical data structures

Sets, sequences and maps are built in, with comprehensions:

let squares = { x * x | x in {1..10} where x mod 2 = 0 }
let ages    = { "alice" -> 31, "bob" -> 27 }

Maps support partial updates, so a model can write ages("alice") := 32 without rebuilding the map, and the update participates in the step’s update set like any other.

Constraints

Assertions, preconditions and type constraints let a model state what must hold rather than checking it defensively:

require balance >= amount

Constraints are what a generated test actually checks. This is the join between AsmL as documentation and AsmL as an oracle: the same statement tells a human what is expected and tells the test harness what to verify.

Structuring

AsmL has classes with mutable instance variables, structures for immutable structured values with named cases (usable in pattern matching), enumerations, interfaces and method overloading. The object model is deliberately the .NET one, so that a model of a component looks like the component.

Evolution

AsmL’s arc is unusual: the language succeeded by being absorbed into a tool and then replaced within it.

The pivot in that table happened around 2003-2004. The published accounts are candid about it: testing with AsmL-T became more popular than AsmL itself. Teams wanted generated tests more than they wanted executable specifications, and the moment the tool mattered more than the language, the language’s specific syntax became negotiable. When the next generation of Spec Explorer arrived, it dropped AsmL in favour of C# and Spec# - notations developers already knew - and kept the underlying exploration machinery.

Spec# is the clearest surviving descendant of the ideas. It extended C# with preconditions, postconditions, object invariants and non-null types, drawing on JML and Eiffel, and it came out of the same Microsoft Research milieu that produced AsmL. The lesson Microsoft Research appears to have drawn from AsmL is that contracts embedded in the implementation language get adopted, while a separate specification language, however well designed, does not.

Running AsmL Today

There is no Docker image, no package manager entry, and no modern toolchain for AsmL - hence the empty Docker section on this page. What survives is:

• The installer. AsmL for Microsoft .NET was distributed as a small MSI, reportedly labelled version 2.2.4382. Where Microsoft download listings for it survive, the dates shown reflect the download centre’s own republication rather than the age of the software - the language itself is a mid-2000s artefact.
• Spec Explorer distributions, which Microsoft Research described as the route by which the AsmL compiler binaries were shipped; the Spec Explorer 2010 line ended with release 3.5.3146.0 on July 8, 2013.
• The documentation, which is in better shape than the software. Introducing AsmL: A Tutorial for the Abstract State Machine Language and the reference manual AsmL: The Abstract State Machine Language are both still mirrored on university course pages.

The sources were released as a community project on CodePlex in 2009, but CodePlex was shut down by Microsoft in 2017, so that route now requires digging through archives. Anyone attempting to run AsmL should expect a Windows machine with an older .NET Framework, and should treat the exercise as archaeology rather than development. The Word add-in in particular ties the literate-programming workflow to a specific era of Office.

Current Relevance

AsmL is dormant, and has been for the better part of two decades. Nothing is built in it today.

Its ideas are not dormant. Abstract state machines remain an active research formalism, and the ASM community continues to produce tools - ASMETA and CoreASM among them - that pursue the same goal of executable, refinable formal models. Model-based testing, which AsmL and AsmL-T did a great deal to make concrete inside a large software company, is now a recognised discipline with its own tools and literature.

The more direct inheritance runs through Microsoft’s own subsequent work: Spec#, Code Contracts, and the general move to express specification inside the implementation language rather than beside it. Those efforts learned AsmL’s lesson - that adoption follows the path of least resistance from the code developers already write.

Why It Matters

It was a real industrial test of executable specification. Most formal specification languages are evaluated in universities on problems chosen to suit them. AsmL was aimed at Windows components and .NET libraries, used by test teams under shipping deadlines, and its results were published including the parts that did not go as planned. That makes it unusually informative.

It showed that the tool beats the notation. AsmL’s designers built an elegant language and discovered that what the organisation wanted was the test generator attached to it. When the notation was swapped for C#, the value survived. This is a recurring, uncomfortable pattern in formal methods, and AsmL is one of the best-documented instances of it.

It took the document seriously. The Word integration looks quaint now, but the underlying idea - that a specification has to live where the people who need it already work, and that prose and executable content belong in one artefact - is exactly the argument later made by literate notebooks and executable documentation. AsmL made it in 2002, for a Word document, aimed at program managers.

It connected theory to a compiler. The ASM thesis is a genuinely deep claim about computation, and AsmL is what happened when someone tried to make a .NET compiler out of it. The Semantic Essence of AsmL paper, published in Theoretical Computer Science in 2005, closed the loop by giving the shipped language a formal semantics. Very few industrial languages of any era have that lineage in both directions.