## FM-SEET 2015: Mathematical Reasoning Elementary Concept Inventory Test II |

## Terminology and Notations

*** Please keep a copy of the following information ***

.
**Terminology:**
• A *requires clause* is an operation’s precondition.
• An* ensures clause* is an operation’s postcondition.
• A loop invariant is an assertion that is true at the beginning and end of each iteration of the loop body
.
**Notations:**
• In the ensures clause, *#Q* denotes the incoming value of a parameter *Q*

• Concatenation of (abstract string or sequence) values of two queues* P* and *Q* is denoted by *P o Q*.

• To concatenate a single entry *E*, the notation* <E>* is used.

• Length of (the abstract string or sequence value of) a queue *Q* is denoted by *|Q|*.

*** Please keep a copy of the following information ***

.

**Terminology:**

*requires clause*is an operation’s precondition.

*ensures clause*is an operation’s postcondition.

**Notations:**

*#Q*denotes the incoming value of a parameter

*Q*

• Concatenation of (abstract string or sequence) values of two queues

*P*and

*Q*is denoted by

*P o Q*.

• To concatenate a single entry

*E*, the notation

*<E>*is used.

• Length of (the abstract string or sequence value of) a queue

*Q*is denoted by

*|Q|*.