Specifying a contract

(NOTE: this page is still under construction. Please contact us if you have any questions.)

In BeepBeep's terminology, a contract is anything that gives a constraint to the sequence of XML messages, their data content, or a mixture of both. A contract can be broken down into a number of properties; typically, one wishes that all these properties remain true at all times during the execution.

BeepBeep's language: Linear Temporal Logic

The contract properties in BeepBeep are expressed as formulas in an extension of Linear Temporal Logic (LTL), called LTL-FO+. The semantics of this logic is defined on a trace (i.e. a sequence) of XML messages being sent or received; the content of these messages is accessible through (simple) XPath expressions and can be stored into variables for future use.

Accessing message contents

Data inside a message can be accessed using first-order quantifiers:

  1. x ∈ π means "for every x in π". Here, x is a variable, and π is a path expression used to fetch possible values for x. For example, if φ is a formula where x appears, then x/tag1/tag2 : φ means: every value at the end of /tag1/tag2 satisfies φ.
  2. x ∈ π means "some x in π". Hence, x ∈ /tag1/tag2 : φ means: there exists some value at the end of /tag1/tag2 which satisfies φ.

For example, consider the following XML message:

<message>
  <action>login</action>
  <username>frank</username>
  <books-return>
    <book>123</book>
    <book>456</book>
    <book>789</book>
  </books-return>
  <books-borrow>
    <book>321</book>
    <book>456</book>
  </books-borrow>
</message>

To express the fact that the action element of this message contains the value login, one can write in LTL-FO+:

x ∈ /message/action : x = "login"

The previous formula says literally: in the current message, there exists a value x at the end of the path /message/action such that x = "login".

LTL-FO+ provides all the familiar Boolean connectives: ∧ ("and"), ∨ ("or"), ¬ ("not"), → ("if then"). They can be used to combine expressions as usual. For example, to express the fact that the book with ID 444 is not present in the current message, one can write:

x ∈ /message/books-return/book : ¬ (x = "444")

This reads as: in the current message, every value x at the end of the path /message/books-return/book is not equal to 444.

One can quantify multiple times to compare different values in the current message. For example:

x ∈ /message/books-return/booky ∈ /message/books-borrow/book :  ¬ (x = y)

In English: for every x at the end of /message/books-return/book, and every y at the end of /message/books-borrow/book, we never have that x = y; in other words, the returned books must be different from the borrowed books. (This would be false in the previous message, as 456 appears in both sides.)

Sequences of messages

Properties can then be defined on sequences of messages using the following LTL temporal operators (see also Wikipedia):

  1. X means "in the next message". For example, if φ is a formula, X φ says that φ will be true in the next message.
  2. G means "globally". For example, if φ is a formula, G φ says that φ is true in the current message, and will be true for all remaining messages in the trace.
  3. F means "eventually". Writing F φ says that φ is either true in the current message, or will become true for at least one message in the future.
  4. U means "until". If φ and ψ are formulas, writing φ U ψ says that ψ will be true messageually, and in the meantime, φ is true for every message until ψ becomes true.

For example, in order to say that "a user must eventually log out", one can write:

F (∃x ∈ /message/action : x = "logout")

The previous formula says: eventually, some message in the trace will fulfill the condition that some tag at the end of path /action will have the value "logout".

To say that borrowed books and returned books are never the same, one can take the formula shown previously, and enclose it within a G operator, yielding:

G (∀x ∈ /message/books-return/booky /message/books-borrow/book :  ¬ (x = y))

It is also possible for a variable to keep its value across be reused at a later time in the trace. For example:

G (∀x ∈ /message/books-borrow/book :  F (∀y ∈ /message/books-return/book : x = y))

This formula says that globally, every book appearing in the section books-borrow of some message must eventually reappear in some future message in the books-return section. Here, the value of x is retrieved in some message, and reused in a future message. This capability of freely mixing temporal operators and quantifiers makes LTL-FO+ a very powerful language to express constraints on sequences of XML messages.

These operators can be nested or combined with traditional boolean connectives to create compound statements.

The contract file

By default, BeepBeep looks for a file called beepbeep-contract.txt located in the same directory as beepbeep.js. This file can contain comments, properties and captions for these properties. The following syntax is accepted:

Special LTL-FO+ symbols, such as and , have an equivalent notation in text files. A formula such as x ∈ /a/b/c : φ is written as:

[x /a/b/c] (φ)

Similarly, x ∈ /a/b/c : φ is written as:

<x /a/b/c> (φ)

The operators ∧ ("and"), ∨ ("or"), ¬ ("not"), → ("if then") respectively translate into &, |, ! and ->.

See, for example, the contract file for the simple library example, taken from the quick demo tour.

Take extra care in enclosing any sub-expression into parentheses (including single variables). The BeepBeep parser is very picky.

Other input methods

We are currently working on a tool to translate UML Sequence Diagrams into LTL-FO+. It should be available in the first weeks of 2009 some time soon.

Main menu

SourceForge.net Logo