|
| 1 | +:tocdepth: 1 |
| 2 | + |
| 3 | +.. index:: signature |
| 4 | + |
| 5 | +.. _signatures: |
| 6 | + |
| 7 | +Signatures |
| 8 | +########## |
| 9 | + |
| 10 | +Parameterized modules use signatures as a type system for their parameters. |
| 11 | +There are three categories of signatures: **predicate signatures**, **type signatures**, and **module signatures**. |
| 12 | + |
| 13 | +Predicate signatures |
| 14 | +==================== |
| 15 | + |
| 16 | +Predicate signatures declare module parameters that will be substituted with predicates when the module is instantiated. |
| 17 | + |
| 18 | +The substitution of predicate signatures relies on structural typing. That is, predicates do not have to be explicitly |
| 19 | +defined as implementing a predicate signature - they just have to match the return and argument types. |
| 20 | + |
| 21 | +Predicate signatures are defined much like predicates themselves, but they do not have a body. |
| 22 | +In detail, a predicate signature definition consists of: |
| 23 | + |
| 24 | +#. The keyword ``signature``. |
| 25 | +#. The keyword ``predicate`` (allows subsitution with a :ref:`predicate without result <predicates-without-result>`), |
| 26 | + or the type of the result (allows subsitution with a :ref:`predicate with result <predicates-with-result>`). |
| 27 | +#. The name of the predicate signature. This is an `identifier <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#identifiers>`_ |
| 28 | + starting with a lowercase letter. |
| 29 | +#. The arguments to the predicate signature, if any, separated by commas. |
| 30 | + For each argument, specify the argument type and an identifier for the argument variable. |
| 31 | +#. A semicolon ``;``. |
| 32 | + |
| 33 | +For example: |
| 34 | + |
| 35 | +.. code-block:: ql |
| 36 | +
|
| 37 | + signature int operator(int lhs, int rhs); |
| 38 | +
|
| 39 | +Type signatures |
| 40 | +=============== |
| 41 | + |
| 42 | +Type signatures declare module parameters that will be substituted with types when the module is instantiated. |
| 43 | +Type signatures are used to specify supertypes and are the simplest category of signatures. |
| 44 | + |
| 45 | +The substitution of type signatures relies on structural typing. That is, types do not have to be explicitly defined as |
| 46 | +implementing a type signature - they just need to have the specified (transitive) supertypes. |
| 47 | + |
| 48 | +In detail, a type signature definition consists of: |
| 49 | + |
| 50 | +#. The keyword ``signature``. |
| 51 | +#. The keyword ``class``. |
| 52 | +#. The name of the type signature. This is an `identifier <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#identifiers>`_ |
| 53 | + starting with a uppercase letter. |
| 54 | +#. Optionally, the keyword ``extends`` followed by a list of types, separated by commas. |
| 55 | +#. A semicolon ``;``. |
| 56 | + |
| 57 | +For example: |
| 58 | + |
| 59 | +.. code-block:: ql |
| 60 | +
|
| 61 | + signature class ExtendsInt extends int; |
| 62 | +
|
| 63 | +Module signatures |
| 64 | +================= |
| 65 | + |
| 66 | +Module signatures declare module parameters that will be substituted with modules when the module is instantiated. |
| 67 | +Module signatures specify a collection of types and predicates that a module needs to contain under given names and |
| 68 | +matching given signatures. |
| 69 | + |
| 70 | +Unlike type signatures and predicate signatures, the substitution of type signatures relies on nominal typing. |
| 71 | +That is, the definition of a module must declare the module signatures it implements. |
| 72 | + |
| 73 | +In detail, a type signature definition consists of: |
| 74 | + |
| 75 | +#. The keyword ``signature``. |
| 76 | +#. The keyword ``module``. |
| 77 | +#. The name of the module signature. This is an `identifier <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#identifiers>`_ |
| 78 | + starting with a uppercase letter. |
| 79 | +#. Optionally, a list of parameters for :ref:`parameterized module signatures <parameterized-module-signatures>`. |
| 80 | +#. The module signature body, consisting of type signatures and predicate signatures enclosed in braces. |
| 81 | + The ``signature`` keyword is omitted for these contained signatures. |
| 82 | + |
| 83 | +For example: |
| 84 | + |
| 85 | +.. code-block:: ql |
| 86 | +
|
| 87 | + signature module MSig { |
| 88 | + class T; |
| 89 | + predicate restriction(T t); |
| 90 | + } |
| 91 | +
|
| 92 | + module Module implements MSig { |
| 93 | + newtype T = A() or B(); |
| 94 | +
|
| 95 | + predicate restriction(T t) { t = A() } |
| 96 | + } |
| 97 | +
|
| 98 | +.. _parameterized-module-signatures: |
| 99 | + |
| 100 | +Parameterized module signatures |
| 101 | +------------------------------- |
| 102 | + |
| 103 | +Module signatures can themselves be parameterized in exactly the same way as parameterized modules. |
| 104 | +This is particularly useful in combination with the dependent typing of module parameters. |
| 105 | + |
| 106 | +For example: |
| 107 | + |
| 108 | +.. code-block:: ql |
| 109 | +
|
| 110 | + signature class NodeSig; |
| 111 | +
|
| 112 | + signature module EdgeSig<NodeSig Node> { |
| 113 | + predicate apply(Node src, Node dst); |
| 114 | + } |
| 115 | +
|
| 116 | + module Reachability<NodeSig Node, EdgeSig<Node> Edge> { |
| 117 | + Node reachableFrom(Node src) { |
| 118 | + Edge::apply+(src, result) |
| 119 | + } |
| 120 | + } |
0 commit comments