AsmL是一种以抽象状态机（Abstract State Machines, ASM）为基础的软件规格语言。它由微软研究院的软件工程基础小组开发并维护，目前的版本是AsmL2（AsmL for microsoft.NET），此版本能够嵌入Microsoft word 和Microsoft Visual Studio.NET中，并可在.NET环境下编译执行。你可以在以下地址找到它：http://research.microsoft.com/foundations/asml/XML:namespace prefix = o ns = "urn:schemas-microsoft-com:Office:office" />

AsmL通过规模最小的但是完整的方法创建一个系统操作的人类可读（Human-readable）、机器可执行（Machine-executable）的模型，这种方法与任何给定的用户级别的抽象相关。这种用AsmL写成的规格被称为可执行规格（executable specification）。

可执行规格具有几个非凡的特性：

首先，AsmL模型可以作为他们所描述的系统的模拟程序来运行。这意味着开发团队甚至可以在没有写任何代码之前，就能够检查他们的设计与预期的有什么不同。然而，AsmL模型并不仅仅是个原型系统或者参考实现，因为它完整地描述了所选设计级别的细节。换句话说，一个适当构建的AsmL模型能够告诉我们，一个正确的实现必须（must）做什么，可以（may）做什么以及不能（must not）做什么。

其次，AsmL模型能够与它所描述的系统的实现并行执行，以检查实现与规格是否相符。这不但可以检查实现，同时可以保证规格及时更新。

第三，AsmL对算法测试用例以及大部分用例中的模型检查和认证有严格的要求。

如同传统的软件规格，可执行规格也描述软件组件如何工作。但与传统规格不同的是，可执行规格具有单一的、明确的含义。这个含义以抽象状态机、系统发展的数学模型、运行时状态的形势呈现。

举例来说，AsmL规格可以作为程序运行来模拟一个系统如何动作，或者检查一个实现的行为是否与规格相符。然而，与传统的程序不同，可执行规格有意保持最小规模。换句话讲，虽然他们的描述很详实，却不冗长，所有的东西都是所选的详细级别的一部分。

因此，与传统的程序不同，可执行规格用来限定它们自身的约束和行为，是系统中所有正确实现所具有的共同的约束和行为。举例来说，可执行规格并不限制操作的顺序，除非顺序具有重要的意义。而传统程序却将操作的命令序列作为实现时的关键决定。可以通过下面这个例子观之：

In-place sorting

var A = [3, 10, 5, 7, 1]

indices = {0, 1, 2, 3, 4}

Main()

  step until fixpoint

  choose i in indices, j in indices

   where i < j and A(i) > A(j)

  A(i) := A(j)

  A(j) := A(i)

  step

  WriteLine(A)  // prints [1, 3, 5, 7, 10]

这个可执行规格使用一个抽象状态机通过single-swap算法实现In-place sorting。

机器执行一系列顺序的步骤来交换A中的值。A中的元素由索引i和j表示，使得i小于j并且A(i)大于A(j)。交换持续进行，直到条件不成立，也就是说，整个序列按序排列为止。最后一步打印排列好的序列。每一步的机器状态完全由那一步时的A序列的值决定。

规格的规模是最小的。首先，choose表达式并没有说如何选择两个索引，只是限定无论两个索引如何选择，必须满足i < j并且A(i)>A(j)。因此，许多排序算法，包括快速排序和冒泡排序，都与我们的规格是一致的。其次，这个例子也没有说如何交换两个元素，而是将如何实现有序的交换留给每一个实现去决定。

总的说来，AsmL规格对于团队的设计决策交流来说是一种理想的方式。同时，程序经理、开发人员以及测试人员都可以使用AsmL规格来达到对设计的单一而统一的理解。