How to use propositions and quantifiers in system specifications

System specifications

System specifications demonstrate the requirements of a system and work as a mindmap for software engineers during the system development phase. System and software engineers take the requirements in natural language. Translating them into logical expressions is essential in producing hardware and software systems specifications.

Propositions and quantifiers

Logical propositions and quantifiers prove beneficial in representing system specifications.

Let’s see how we can logically express specifications in the following examples.

Example 1

Let’s express the following specification using logical connectives:

• $s$: The user cannot log in when the password is incorrect.

Here is one way to translate this. Consider:

• $p$: The user can log in.
• $q$: The password is incorrect.

Now:

• $\neg p \equiv$ The user cannot log in.

Subsequently, we can represent the specification by the conditional statement $q \Rightarrow \neg p$.

Example 2

For the following example, we’ll use predicates and quantifiers to express the given two system specifications.

• $s_1$: Every username containing more than two underscores will be considered invalid.
• $s_2$: If a user is logged in, all the available features will be shown.

Let $Q$ and $I$ be two predicates for the first specification $s_1$.

• $Q(u, y)$: The username $u$ contains more than $y$ underscores, where $u$ has the domain of all the usernames, and $y$ is a positive integer.
• $I(u)$: The username $u$ will be considered invalid.

Then, we can represent the specification $s_1$ as follows:

$$\forall u (Q(u, 2) \Rightarrow I(u)).$$

For the second specification, $s_2$, consider the following predicates:

• $U(x)$: User $x$ is logged in, where $x$ has the domain of all the users.
• $F(y)$: The feature $y$ is shown to the user, where $y$ has the domain of all the features.

Then we can represent the specification $s_2$ as follows:

$$\exists x U(x) \Rightarrow \forall y F(y).$$

Consistency of specifications

One of the significant benefits of translating system specifications into logical expressions is to check for the consistency of specifications. That is, there should not be any conflicting requirements. We can use compound propositions and quantifiers to express the specifications and then find an assignment of truth values that make all the specifications true. Consequently, we can develop a system that satisfies all the requirements.