Reference¶
Overview¶
Apilog is a logic programming language for documenting and testing RPC interfaces. The language has three fundamental syntactical categories: types, expressions, and actions. In addition, it has syntax for defining predicates, APIs, issuing commands and more. Rather than giving a detailed grammar for all the syntax up front, this document will take you on a tour around the main concepts of Apilog, explaining some of the syntactical elements on the go. It is work in progress and currently lacks a description how to define data types as well as a deeper description of the semantics of the language.
Type system¶
The type system of Apilog is fairly standard and behaves like most polymorphic
type systems for functional programming. There are function types, written
using the function arrow syntax (->) and there is a type for logical
formulas, called prop. Then there is a bunch of simple data types such as
string, int, etc. There are also parameterised types besides functions
types. For example, the type of lists of integers is written list int.
Moreover, since the type system is polymorphic, types can contain variables,
written using capitalized identifiers. For example, the type of a predicate
that checks for list membership can be written A -> list A -> prop. Finally,
specification authors can declare new types, as we shall see later.
Expressions¶
Expressions are similar to expressions in functional languages. Function
application is written f x. The syntax for lambda abstraction is a bit
unusual, however. It is written X\ e, where X is the bound variable and e
is some expression.
Actions¶
The action language is used to describe interactions with an API. It contains syntax for sequencing actions, running actions in parallel, making remote procedure calls, and testing the result of actions. However, apilog specifications can only directly use the syntax for making remote procedure calls. The rest of the action language is only used to describe the actions that Apilog took during testing, and can be shown in the user interface, but not written in the specification itself. Morever, even though actions is a separate syntactical category from expressions, actions can be wrapped as expressions (using a special expression syntax element). This wrapping makes it possible to define short-form constants that describe actions, and include actions in formulas. Specifications will mostly use short-form action expressions from the Apilog library, some of which are:
get : path -> list (tuple string string) -> action http_response
post : path -> list (tuple string string) -> string -> action http_response
put : path -> list (tuple string string) -> string -> action http_response
delete : path -> list (tuple string string) -> action http_response
The path arguments represent URI paths, the lists of tuples represent HTTP headers and the string arguments represent HTTP request bodies.
Formulas and terms¶
The connectives in the Apilog logic are encoded as expression constants,
which means that logical formulas are simply expressions (of type prop).
There are certain restrictions in place that prevent logical formulas from
quantifiying over logical formulas, in order to make the logic first-order.
For this reason we must also talk about terms, the subset of expressions that
does not contain formulas.
Resource declarations¶
The concept of a resource is central to Apilog. A resource represents
something that exists in the system behind the API, and that can typically be
manipulated via the API. Resources are encoded as logical predicates (applied
to all their arguments). New such resource constants can be declared with the
resource keyword, followed by a name and a type. Here is an example:
resource user : string -> prop.
The above declaration says that there is a predicate constant called user
with a string argument, and that this predicate (when applied to its argument
and used in a logical formula) represents a resource. In this example, the
string argument could represent the user name.
Positive formulas¶
Positive formulas are used to generate data as well as to express pre- and post-conditions. They follow this abstract grammar:
where \(P\) stands for atoms and \(t\) for terms.
Atoms¶
An atom is a non-logical constant applied to all its arguments. As such, it is a formula that does not contain any logical constants. There are two kinds of atoms: resource atoms and built-in atoms.
Resource atoms¶
In a resource atom, the constant must have been declared as a resource. For
example, if a constant user : string -> prop has been declared, user "x"
would be a resource atom, which could represent the assumption that the user
named "x" exists in the system behind the API.
Built-in atoms¶
In a built-in atom, the constant refers to a procedure that is built-in to the
Apilog interpreter. An example of such a constant is parse_json : string ->
json -> prop.
Multiplicative conjunction¶
\(\tensor\) is the multiplicative conjunction connective from linear logic. It
can be thought of as a version of "and" that can represent the simultaneous
occurence of resources. In the concrete syntax, it is written , (comma), like
conjunction in Prolog. Also like in Prolog, interpretation proceeds
left-to-right.
One¶
\(\one\) is the unit of \(\tensor\) from linear logic, and is written one in the
concrete syntax. It represents the absence of resources and can be thought of
as a version of "true" from more standard logics.
Additive disjunction¶
\(\adisj\) is the additive disjunction connective from linear logic. It can be thought of as a version of "or" that can represent non-deterministic choice between resources. It is written in the concrete syntax with ';' (semi-colon), like disjunction in Prolog.
When the Apilog interpreter finds this connective in a goal (pre-condition), it makes a randomized choice of which branch to try first, and performs chronological backtracking upon failure. It does not try to find multiple solutions.
When the Apilog intepreter finds this connective in a hypothesis (post-condition), it tries the first branch and then the second. If there is more than one solution, it yields a "fatal error", indicating an error in the specification. In effect, specifications are required to be deterministic.
Zero¶
\(\zero\) is the unit of \(\adisj\) from linear logic and is written zero in the
concrete syntax. It represents a resource that cannot be produced and can be
thought of as a version of "bottom" or "false" from more standard logics.
Existential quantification¶
\(\exists x.A^+\) is existential quantification. In concrete syntax, it can be
written using the built-in constant exists : (A -> prop) -> prop. For
example: exists (X\ e) where e is some expression typically containing X.
The quantified variable must be of term type.
Equality¶
\(=\) is term equality, written = in concrete syntax.
Recursion¶
Positive formulas can be recursive using the the fixed point combinator \(\mu\). In the surface syntax, this combinator is not available. Instead, recursion is achieved by making a definition that refers to itself. This self-reference is then translated into an application of the fixed-point combinator.
Negative formulas¶
Negative formulas are used to describe APIs. They follow this abstract grammar:
Additive conjunction¶
\(\with\) is the additive conjunction connective from linear logic. It is used to
represent a (client-side) choice between APIs. It can be thought of as a
version of "and" from more standard logics, and is written & in the concrete
syntax.
Top¶
\(\top\) is the unit of \(\with\) from linear logic and is written top in the
concrete syntax. It is used to represent the empty API and can be thought of as
version of "true" from more standard logics.
Universal quantification¶
\(\forall x.A^-\) is universal quantification. In concrete syntax, it can be
written using the built-in constant forall : (A -> prop) -> prop. For
example: forall (X\ e) where e is some expression typically containing X.
The quantified variable must be of term type.
Linear implication¶
\(\limp\) is the linear implication arrow from linear logic, written -o in the
concrete syntax. It can be seen as a resource-aware version of logical
implication. The antecedent (the left argument) must be a positive formula,
which can contain resources, and the consequent (the right argument) must be a
negative formula. When a linear implication is used to prove its consequent,
the resources in the antecedent are consumed.
Action modality¶
\(\langle a \rangle x.A^+\) is a modal formula that means that the formula \([t/x]A^+\) is true after action \(a\) has happened, if term \(t\) is the result of \(a\).
The concrete syntax is:
{a}f
where a is an action of type action r, and f a function of type r ->
prop (more precisely, a function from the result of the action to a positive
formula). For example:
{get /users/U _ _ _}(R\ status 200 R, user U)
Resources in the formula returned by f (like user U in the above example)
are added to the set of assumptions about the system under test, after the
action a is performed, during testing. Note that status 200 R in this
example is not a resource atom, but a defined atom (which will be explained
later).
Definitions¶
As alluded to earlier, Apilog allows definitions of contants. A definition is a top-level statement that declares a new constant and assigns it a logical formula. Internally, such atoms are substituted by their definitions which explains why they are not present in the abstract syntax (as presented in the sections on positive and negative formulas).
There are two kinds of definitions: API definitions and predicate definitions.
API definitions¶
API definitions are made with the api keyword, like in the following example:
api get_user := user U -o {get /users/U _ _ _}(R\ status 200 R, user U).
The right hand side (right of :=) is always a negative logical formula.
Variables and quantification¶
Any unbound and capitalized identifier in the formula (like U in the
example) is implicitly universally quantified. I.e. there is a hidden forall-
quantifier for U at the start of the formula in the example. Also, note that
in the example above, the variable R is not implicitly quantified as it is
bound as an argument to an anonymous function.
API clauses¶
In the example above, the formula has a single application of the action modality. Such a formula we call an API clause. We call the modal formula the head of the clause and the antecedent of the linear implication the body of the clause.
Combining APIs¶
APIs can be combined with the & connective. I.e. one can write API
definitions that join multiple APIs together like this:
api main := get_user & delete_user.
One can also write multiple API clauses in one definition:
api main :=
user U -o {get /users/U _}(R\ status 200 R, user U) &
user U -o {delete /users/U _}(R\ status 200 R).
API clause restrictions¶
There are two restrictions on API clauses: they must not overlap and they must have atomic actions.
Non-overlapping API clauses¶
Overlap between API clauses occur when there are two or more clauses with actions that can be "unified" i.e. which can be made equal using a specific substitution of variables. If this occurs, Apilog complains with an error message.
Note that the body of the clause has no effect on whether the heads actions are considered overlapping or not. The unification of head actions is attempted without looking at the bodies.
This restriction is similar to the behaviour of type class instance resolution in Haskell.
Atomic actions¶
Actions in API clauses must be atomic rpc actions. If not, Apilog complains
with an error message.
Rationale¶
There are two reasons for these two restrictions.
1) If API clause are non-overlapping and contain only atomic actions, Apilog never needs to consider more than one API clause in its proof search after having made a remote procedure call.
2) With these restrictions, the actions serve well as documentation headings in the generated API documentation, because the resulting headings are guaranteed to be unique, and likely to be short and summary.
Predicate definitions¶
Predicates can be defined by clauses, with def-by syntax. A type must be
declared and the clauses must be separated by vertical bars (|).
Here is an example of a predicate that checks for list membership:
def elem : A -> list A -> prop by
| elem A [A|_]
| elem A [_|L] := elem A L.
The expression to the left of := is called a head and the expression to
the right a body, the latter which can be omitted. The head must be an atom
with the same predicate constant that is defined (elem in this example). The
body can be any positive formula.
This clause-by-clause definition style mimics horn clauses. The same predicate could look like this in Prolog:
elem(A, [A|_]).
elem(A, [_|L]) :- elem A L.
Clause-by-clause definitions is just a form of syntactial sugar. The Apilog interpreter always "desugars" the clauses into a function from the arguments of the predicate to a single positive logical formula.
Existential quantification¶
All unbound capitalized identifiers in the clauses are implicitly existentially quantified.
Recursion¶
A def-by definition can refer to itself, i.e. it can be recursive. However,
Apilog does not yet support mutual recursion.
Commands¶
Commands are top-level statements prefixed with #, and cause things to
happen. In order to run tests, for example, you need to add a #check command
(see below) to you specification.
#baseuri¶
Syntax¶
#baseuri e.
where e is an expression of type string.
Meaning¶
Sets the base URI that will prefix each path during testing.
Example¶
#baseuri "https://httbin.org".
#check¶
Syntax¶
#check e.
where e is an expression of type prop, i.e. a formula.
The formula must be negative (i.e. an API formula).
Meaning¶
Runs tests against the system at the base URI. In order to generate tests, Apilog does proof search. This search is set up so that the positive API formula in the argument to the command is put in the unrestricted context of the hypothetical judgement to be proved, which means that Apilog is allowed to use the API formula any number of times (i.e. it is not restricted to be used linearly).
Any capitalized and unbound identifier in e is implicitly universally
quantified.
Examples¶
#check {get /foo _ _}(R\ status 200 R).
#check api1 & api2.
#query¶
Syntax¶
#check e.
where e is an expression of type prop, i.e. a formula.
The formula must be positive.
Meaning¶
Does proof search with the goal e. Any capitalized and unbound identifier in
e is implicitly existentially quantified.
Example¶
#query append "foo" "bar" S.