签名¶

参数化模块使用签名作为其参数的类型系统。签名分为三类：**谓词签名**、**类型签名**和**模块签名**。

谓词签名¶

谓词签名声明模块参数，这些参数将在模块实例化时替换为谓词。

谓词签名的替换依赖于结构化类型。也就是说，谓词不必明确定义为实现谓词签名——它们只需匹配返回类型和参数类型即可。

谓词签名的定义方式与谓词本身非常相似，但它们没有主体。具体来说，谓词签名定义包含：

关键字 signature。
关键字 predicate（允许替换为无结果谓词），或结果类型（允许替换为有结果谓词）。
谓词签名的名称。这是一个以小写字母开头的标识符。
谓词签名的参数（如果有），用逗号隔开。对于每个参数，指定参数类型和参数变量的标识符。
分号 ;。

例如

signature int operator(int lhs, int rhs);

类型签名¶

类型签名声明模块参数，这些参数将在模块实例化时替换为类型。类型签名可以指定超类型和必需的成员谓词（除了由超类型隐含的那些成员谓词）。

类型签名的替换依赖于结构化类型。也就是说，类型不必明确定义为实现类型签名——它们只需具有指定的（传递的）超类型和成员谓词即可。

具体来说，类型签名定义包含：

关键字 signature。
关键字 class。
类型签名的名称。这是一个以大写字母开头的标识符。
可选地，关键字 extends 后跟一个类型列表，用逗号隔开。
要么是分号 ;，要么是大括号中包含的谓词签名列表。对于这些包含的签名，signature 关键字被省略。

例如

signature class ExtendsInt extends int;

signature class CanBePrinted {
  string toString();
}

模块签名¶

模块签名声明模块参数，这些参数将在模块实例化时替换为模块。模块签名指定模块在给定名称下需要包含的类型和谓词集合，以及与给定签名匹配的集合。

与类型签名和谓词签名不同，模块签名的替换依赖于名义类型。也就是说，模块的定义必须声明它实现的模块签名。

具体来说，类型签名定义包含：

关键字 signature。
关键字 module。
模块签名的名称。这是一个以大写字母开头的标识符。
可选地，参数化模块签名的参数列表。
模块签名主体，包含大括号中包含的类型签名、谓词签名和默认谓词。对于这些包含的签名，signature 关键字被省略。

模块签名默认谓词在语法上与谓词签名类似，但以 default 关键字开头，并带有谓词主体而不是结尾的分号 ;。默认谓词主体受到限制，它们不能使用以任何方式依赖于其他模块签名成员或模块签名参数或任何现有封闭模块的实体。

例如

signature module MSig {
  class T;
  predicate restriction(T t);
  default string descr(T t) { result = "default" }
}

module Module implements MSig {
  newtype T = A() or B();

  predicate restriction(T t) { t = A() }
}

参数化模块签名¶

模块签名本身可以像参数化模块一样进行参数化。这与模块参数的依赖类型结合起来特别有用。

例如

signature class NodeSig;

signature module EdgeSig<NodeSig Node> {
  predicate apply(Node src, Node dst);
}

module Reachability<NodeSig Node, EdgeSig<Node> Edge> {
  Node reachableFrom(Node src) {
    Edge::apply+(src, result)
  }
}