Exercise Sheet 7, Exercise 13

Hello everyone,

I was just doing the Exercise 13.: Constructing Specifications. I got a bit confused about the equality signs and implications for notating specifications.

Example of my problem

What I want to write mathematically is:

if(n < 0) {
    n = (-1) * n

Which of the following notations is correct? Or are both valid?

(\sigma n \lt 0 \land \sigma\prime n = -\sigma n)

Or is it:

(\sigma n \lt 0 \Rightarrow \sigma\prime n = -\sigma n)

Because both variants are seen in the solutions.

The solutions of Exercise 12.: Writing Specifications for Programs use the LAnd Operator:


while the solutions for Exercise 13. are using the implication:


I hope it’s clear, what my problem is. In my head, both situations are the same.

if the situation is true
      set 'x' equal to 'y'

but the solutions use different notations to express this in specifications.

Thanks in advance,

1 Like

Okay, first of all: thank you very much for your detailled answer.
But this didn’t solve the issue in my head completely.

Here’s why:
You wrote as possible solution for c)
but the exercise sheet solution used the LAnd Operator-Way

Which solution is the better solution?
If I understood you correctly, the implication Is most likely to be understood like the If from C:

((x = y) \Rightarrow statement1) \vee (\neg{(x = y)} \Rightarrow statement2)
Exactly if x is equal to y
       do statement1
and in any other case
       do statement2

So, your solution would be “better”, right? What to prefer?

Thanks again!

Alright, I think that answers my questions and solves my confusions entirely, especially this part

It is completely the same if you say: If x is greater than one A, and otherwise, B.
Or if you say: x is greater than one and A holds, or, x is not greater than one and B holds.

and this part

I would formulate it the other way around:
The if in C is somewhat like an implication:
If the condition holds then something happens.

Thank you very much.