Trusted answers to developer questions
Trusted Answers to Developer Questions

Related Tags

How to use propositions and quantifiers in system specifications

Naima Ali

Grokking Modern System Design Interview for Engineers & Managers

Ace your System Design Interview and take your career to the next level. Learn to handle the design of applications like Netflix, Quora, Facebook, Uber, and many more in a 45-min interview. Learn the RESHADED framework for architecting web-scale applications by determining requirements, constraints, and assumptions before diving into a step-by-step design process.

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:

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

Here is one way to translate this. Consider:

  • pp: The user can log in.
  • qq: The password is incorrect.

Now:

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

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

Example 2

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

  • s1s_1: Every username containing more than two underscores will be considered invalid.
  • s2s_2: If a user is logged in, all the available features will be shown.
Flowchart demonstrating specifications

Let QQ and II be two predicates for the first specification s1s_1.

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

Then, we can represent the specification s1s_1 as follows:

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

For the second specification, s2s_2, consider the following predicates:

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

Then we can represent the specification s2s_2 as follows:

xU(x)yF(y).\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.

RELATED TAGS

Grokking Modern System Design Interview for Engineers & Managers

Ace your System Design Interview and take your career to the next level. Learn to handle the design of applications like Netflix, Quora, Facebook, Uber, and many more in a 45-min interview. Learn the RESHADED framework for architecting web-scale applications by determining requirements, constraints, and assumptions before diving into a step-by-step design process.

Keep Exploring