This version of BeepBeep is no longer actively developed.
This site is kept for archival purposes.
For the latest version, please visit:
https://liflab.github.io/beepbeep-3.

(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.

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.

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

- ∀
*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 φ. - ∃
*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/book`
∀*y* ∈ `/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.)

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

**X**means "in the next message". For example, if φ is a formula,**X**φ says that φ will be true in the next message.**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.**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.**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/book`
∀*y* `/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.

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:

- Empty lines, or lines containing only space characters (tabs, etc.) are discarded
- Whitespace at the beginning of a line is discarded
- Lines beginning with
`#`are comments and are discarded - Lines beginning with
`;`are formulas, expressed in the logic LTL-FO+ (see below). Each formula represents one monitoring property (or "constraint"), and is associated internally with one "watcher" - Lines beginning with
`%`are captions. Captions are used to associate a textual description to the formula on the following line. - Lines that do not begin with neither
`#`,`;`nor`%`are "continuation" lines: they are appended (with a space) to whatever comment, formula or caption is currently being read. This is intended to make the file resistant to adding line breaks (for example, by transmitting through e-mail).

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.

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.