1 Notational Conventions

1.1 Notational Conventions

Notational Conventions Notational Conventions

Slide 1

Notational Conventions

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 1 / 11

1
 Notational Conventions Notational Conventions

Notational Conventions - Ranges and Arrays

Before proceeding, we introduce some helpful notation for describing
ranges and arrays. For natural numbers i, x and y:

i ∈ (x..y) , x<i<y
i ∈ [x..y) , x≤i<y
i ∈ (x..y] , x<i≤y
Slide 2

i ∈ [x..y] , x≤i≤y
This notation has a natural lifting to arrays. For an array a, value v and
natural numbers x and y:

v ∈ a[x..y) , ∃i ∈ [x..y).[ 0 ≤ i < a.length ∧ a[i] = v ]

We can now elegantly describe properties of arrays, for example:

a[x..y) ≤ z , ∀v ∈ a[x..y).[ v ≤ z ]

Note: we usually prefer closed-open intervals, e.g. [x..y) or a[x..y).

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 2 / 11

Some more examples of array properties that we are able to define with the above notation
are:

ˆ a(x..y] ≥ z , ∀v ∈ a(x..y].[ v ≥ z ]

ˆ a[x..y] 6= z , ∀v ∈ a[x..y].[ v 6= z ]

We will see later that using closed-open intervals for array slices is often convenient for
our reasoning.

2
 Notational Conventions Notational Conventions

Notational Conventions - Array Slices

We refer to the closed-open interval a[x..y) as an array slice.

Slide 3

For an array a and natural numbers x and y, we can formally define an

array slice inductively as follows:

 [] if y ≤ x
a[x..y) , a[x+1..y) if x < 0 or x ≥ a.length

a[x] : a[x+1..y) otherwise

Notice how the interval’s values are truncated to the bounds of the array a.

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 3 / 11

Although we rarely use them, we can define the three other types of array intervals (to
match the other number ranges) in terms of our array slice notation.
Specifically:

ˆ a(x..y) , a[x+1..y)

ˆ a(x..y] , a[x+1..y+1)

ˆ a[x..y] , a[x..y+1)

3
 Notational Conventions Notational Conventions

Notational Conventions - Arrays and their Contents

To simplify our notation, we drop the interval bounds when they refer to
the start or end of an array. Thus, for an array a and natural number i:

a[..i) describes the array slice from 0 up to, but not including, i
Slide 4

a[i..) describes the array slice from i up to its end

a[..) describes the whole array

We also need to be able to distinguish the reference to an array from the

array’s contents when making old or pre annotations.

a[..)old or a[..)pre refer to previous values of an array’s contents

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 4 / 11

We will often need to use the array contents annotations a[..)old or a[..)pre , as it is very
common for methods to update (or potentially update) the contents of arrays.

4
 Notational Conventions Notational Conventions

Notational Conventions - Array Shorthands

We introduce several notational shorthands for arrays.

For arbitrary arrays a and b, and value v:

N rOccurs(a[..), v) , | { k | a[k] = v } |
Slide 5

a[..) ∼ b[..) means that the contents of array a are a permutation of

the contents of array b:

a[..) ∼ b[..) , ∀v.[ N rOccurs(a[..), v) = N rOccurs(b[..), v) ]

a[..) ≈ b[..) means that the contents of arrays a and b are identical:

a[..) ≈ b[..) , a.length = b.length

∧ ∀j ∈ [0..a.length).[ a[j] = b[j] ]

We will often refer to ≈ as deep equality.

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 5 / 11

For a set S, the term |S| denotes the cardinality (or size) of the set. So, N rOccurs counts
the number of occurrences of a value v in an array. The definition of ∼ then requires that
both arrays contain the same number of occurrences of each possible value.
The definitions of ∼ and ≈ can also be applied to arbitrary array slices, in which case
they only consider their respective array contents in the given intervals. e.g.
a[1..a.length) ≈ b[1..b.length)
describes two arrays a and b that are identical, except for their first element.

5
 Notational Conventions Notational Conventions

Notational Conventions - Array Operations

We also introduce some notational shorthands for operations on arrays.
For an array a and natural numbers x and y:
P
a[x..y) is the sum of the elements of array a from index x up to
but not including index y:
P Py−1
Slide 6

a[x..y) , k=x a[k]

, a[x] + a[x + 1] + ... + a[y − 1]

Πa[x..y) is the product of the elements of array a from index x up to

but not including index y:

Π a[x..y) , Πy−1
k=x a[k]
, a[x] ∗ a[x + 1] ∗ ... ∗ a[y − 1]
P
Important: a[x..y) and Πa[x..y) are only well-defined for ranges [x..y)
that lie within the bounds of array a.
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 6 / 11

P
Note that the sum of an empty array slice (e.g. a[..0)) is defined to be 0 (the unit of
addition).
Similarly, the product of an empty array slice (e.g.Π a[a.length..)) is defined to be 1 (the
unit of multiplication).

6
 Notational Conventions Notational Conventions

Notational Conventions - Helpful Predicates

We introduce some predicates which will be helpful in upcoming examples.

For arbitrary arrays a and b and natural numbers i and j:

Sorted( a[..) ) means that array a is ordered:

Sorted( a[..) ) , ∀j, k ∈ [0..a.length).[ j ≤ k −→ a[j] ≤ a[k] ]
Slide 7

Swapped( a[..), b[..), i, j ) means that the arrays a and b are identical,
except for the elements at indexes i and j, which have been swapped:
Swapped( a[..), b[..), i, j ) , a.length = b.length
∧ i, j ∈ [0..a.length)
∧ b[i] = a[j] ∧ b[j] = a[i]
∧ ∀k∈[0..a.length)\{i,j}.[ a[k] = b[k] ]

Important: Sorted is only well-defined for an array whose contents are

comparable (such as Integers).
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 7 / 11

We can apply the definition of Sorted to an arbitrary array slice if desired:

ˆ Sorted( a[x..y) ) , ∀j, k ∈ [x..y).[ 0 ≤ j ≤ k < a.length −→ a[j] ≤ a[k] ]

A version of Swapped could also be defined for arbitrary array slices, but the above
version is sufficient for all of our needs in this module.

7
 Notational Conventions Notational Conventions

Notational Conventions - Helpful Functions

We also introduce some functions which will be helpful in upcoming

examples. For an array a:

min( a[..) ) gives the smallest element in the array a:

Slide 8

min( a[..) ) , min{ z | ∃j ∈ [0..a.length). a[j] = z }

max( a[..) ) gives the biggest element in the array a:

max( a[..) ) , max{ z | ∃j ∈ [0..a.length). a[j] = z }

Important: min and max are only well-defined for an array whose
contents are comparable (such as Integers).

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 8 / 11

We can apply these definitions to arbitrary array slices if desired. e.g.

ˆ min( a[x..y) ) , min{ z | ∃j ∈ [x..y).[ 0 ≤ j < a.length ∧ a[j] = z ] }

ˆ max( a[x..y) ) , max{ z | ∃j ∈ [x..y).[ 0 ≤ j < a.length ∧ a[j] = z ] }

8
 Notational Conventions Notational Conventions

Array Lemmas - Deep Equality and Permutation

For all arrays a and b:

Deep Equality Lemmas:

a[..) ≈ b[..) −→ b[..) ≈ a[..) (≈Symm)
Slide 9

a[..) ≈ b[..) ∧ b[..) ≈ c[..) −→ a[..) ≈ c[..) (≈Trans)

a[..) ≈ b[..) −→ a.length = b.length (≈Length)
a[..) ≈ b[..) −→ a[..) ∼ b[..) (≈IsPrm)

Permutation Lemmas:
a[..) ∼ b[..) −→ b[..) ∼ a[..) (∼Symm)
a[..) ∼ b[..) ∧ b[..) ∼ c[..) −→ a[..) ∼ c[..) (∼Trans)
a[..) ∼ b[..) −→ a.length = b.length (∼Length)

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 9 / 11

These Lemmas for deep equality and permutation of arrays allow us to quickly deduce
helpful related properties as well as treating both ≈ and ∼ as equality relations.

9
 Notational Conventions Notational Conventions

Notational Conventions - Array Concatenation

We define the concatenation of arrays (:) via their deep equality relation
Slide 10

with a third “observer” array. That is, for arbitrary arrays a, b and c we
have:

a[..) ≈ b[..) : c[..) , a[..b.length) ≈ b[..) ∧ a[b.length..) ≈ c[..)

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 10 / 11

Notice that from the definition of ≈ we know that when a[..) ≈ b[..) : c[..)
then a.length = b.length + c.length
Another, equivalent, but longer, definition of concatenation would be:
a[..) ≈ b[..) : c[..) , a.length = b.length + c.length
∧ ∀i ∈ [0..b.length).[ a[i] = b[i] ]
∧ ∀i ∈ [0..c.length).[ a[i + b.length] = c[i] ]

Using deep equality, array slices and concatenation we can describe many interesting
properties of arrays. For example:
a[..) ≈ a[0..1) : b[..) : a[b.length + 1..a.length)
says that the contents of the array a from index 1 to index b.length is the same as the
array b. It does not say anything about the other elements of the array a. This notation
can be very useful for describing changes to just part of an array, or even for specifying
which parts of an array are unmodified.

10
 Notational Conventions Notational Conventions

Array Lemmas - Swapping and Ranges

For all arrays a and b and for all integers i, j, k, x and y:
Swapped Lemmas:
Swapped(a[..), b[..), i, i) −→ a[..) ≈ b[..) (≈Swpd)
Swapped(a[..), b[..), i, j) −→ a[..) ∼ b[..) (∼Swpd )
Slide 11

Swapped(a[..), b[..), i, j) ←→ Swapped(a[..), b[..), j, i)

←→ Swapped(b[..), a[..), i, j) (SwpSm)
Ranges Lemmas:
b[..) ≈ a[0..i) : b[i..j) : a[j..) ∧ x ≤ i ∧ j ≤ y
−→ b[..) ≈ a[0..x) : b[x..y) : a[y..) (RngWeak)
b[..) ≈ a[0..i) : b[i..j) : a[j..) ∧ a[i..j) ∼ b[i..j)
−→ a[..) ∼ b[..) (RngPrm)
a[..) ≈ b[..) ∧ c[..) ≈ c[0..i) : a[i..j) : c[j..)
−→ c[..) ≈ c[0..i) : b[i..j) : c[j..) (RngSwap)
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 11 / 11

In RngWeak the premise says a and b are identical except for the range [i..j), and the
conclusion says that a and b are identical except for the range [m..n). The lemma holds,
since the range [m..n) includes the range [i..j). We can prove this Lemma as follows:
Given:
(1) b[..) ≈ a[0..i) : b[i..j) : a[j..)
(2) x ≤ i ∧ j ≤ y
To Show:
(α) b[..) ≈ a[0..x) : b[x..y) : a[y..)
Proof:
From (1) and the definition of concatenation we have:
(3) b.length = i + (j − i) + (a.length − j)
(4) ∀k ∈ [0..i). b[k] = a[k]
(5) ∀k ∈ [j..a.length). b[k] = a[k]
From (3) we obtain by arithmetic:
(6) b.length = a.length
From (4), (2) and since x ≤ i ∧ k ≤ x −→ k ≤ i, we obtain:
(7) ∀k ∈ [0..x). b[k] = a[k]
Similarly, from (5) and (2) we obtain:
(8) ∀k ∈ [y..a.length). b[k] = a[k]
From (6), (7) and (8) and definition of concatenation (:), we obtain (α).

11