CSE331�Lecture 2

Reasoning about Loops + HTML

​

​

​

​

​

​

Ardi Madadi �Summer 2021�(Based on slides by Kevin Zatloukal, Mike Ernst, Dan Grossman, and many others)

1

Hoare Logic

A Hoare triple is two assertions and one piece of code:

{{P}} S {{Q}}

• P the precondition
• S the code
• Q the postcondition

​

2

Hoare Logic

A Hoare triple {{ P }} S {{ Q }} is called valid if:

• In any state where P holds,�executing S produces a state where Q holds
• i.e., if P is true before S, then Q must be true after it
• Otherwise, the triple is called invalid
• Code is correct iff triple is valid

​

​

​

3

Reasoning Forward & Backward

A Hoare triple {{ P }} S {{ Q }} is called valid if:

• In any state where P holds,�executing S produces a state where Q holds
• i.e., if P is true before S, then Q must be true after it
• Otherwise, the triple is called invalid
• Code is correct iff triple is valid

​

​

​

4

Reasoning: Assignments

x = expr

Forward

• add the fact “x = expr” to what is known
• BUT you must fix any existing references to “x”

Backward

• just replace any “x” in the postcondition with expr (substitution)

5

Reasoning: Assignments

Forward reasoning

{{ P }}

if (cond)

{{ P and cond }}

S1

{{ P1 }}

else

{{ P and not cond }}

S2

{{ P2 }}

{{ P1 or P2 }}

​

Backward reasoning

{{ cond and Q1 or

not cond and Q2 }}

if (cond)

{{ Q1 }}

S1

{{ Q }}

else

{{ Q2 }}

S2

{{ Q }}

{{ Q }}

​

​

6

Validity with Fwd & Back Reasoning

Reasoning in either direction gives valid assertions

Just need to check adjacent assertions:

• top assertion must imply bottom one

​

{{ P }}

S1

S2

{{ P1 }}

{{ Q }}

{{ P }}

{{ Q1 }}

S1

S2

{{ Q }}

{{ P }}

S1

{{ P1 }}

{{ Q1 }}

S2

{{ Q }}

Reasoning So Far

• “Turn the crank” reasoning for assignment and if statements�
• All code (essentially) can be written just using:
• assignments
• if statements
• while loops
• Only part we are missing is loops

8

Reasoning About Loops

• Loop reasoning is not as easy as with “=“ and “if”
• recall Rice’s Theorem (from 311): checking any non-trivial semantic property about programs is undecidable�
• We need help (more information) before the reasoning again becomes a turn-the-crank process

​

• That help comes in the form of a “loop invariant”

​

9

Loop Invariant

A loop invariant is an assertion that holds at the top of the loop:

​

{{ Inv: I }}

while (cond)

S

​

• It holds when we first get to the loop.
• It holds each time we execute S and come back to the top.

​

Notation: I’ll use “Inv:” to indicate a loop invariant.

10

Loop Invariant

A loop invariant is an assertion that holds at the top of the loop:

​

{{ Inv: I }}

while (cond)

S

​

• It holds when we first get to the loop.
• It holds each time we execute S and come back to the top.

​

Notation: I’ll use “Inv:” to indicate a loop invariant.

11

Lupin Variants

Loop Invariant

Consider a while-loop (other loop forms not too different)�with a loop invariant I. Let’s try forward reasoning...

​

12

{{ P }}

S1

{{P1}}

{{ Inv: I }}

while (cond)

{{ Inv: I }}

S2 {{P2}}

{{ I and not cond }}

S3

{{P3}}

{{ Q }}

​

Loop Invariant

Consider a while-loop (other loop forms not too different)�with a loop invariant I. Let’s try forward reasoning...

​

Need to check that P1 implies I

(i.e., that I is true the first time)

13

{{ P }}

S1

{{P1}}

{{ Inv: I }}

while (cond)

{{ Inv: I }}

S2 {{P2}}

{{ I and not cond }}

S3

{{P3}}

{{ Q }}

​

Loop Invariant

Consider a while-loop (other loop forms not too different)�with a loop invariant I. Let’s try forward reasoning...

​

Need to check that P2 implies I again

(i.e., that I is true the each time around)

14

{{ P }}

S1

{{P1}}

{{ Inv: I }}

while (cond)

{{ I and cond }}

S2 {{P2}}

{{ I and not cond }}

S3

{{P3}}

{{ Q }}

​

Loop Invariant

Consider a while-loop (other loop forms not too different)�with a loop invariant I. Let’s try forward reasoning...

​

Need to check that P3 implies Q

(i.e., Q holds after the loop)

15

{{ P }}

S1

{{P1}}

{{ Inv: I }}

while (cond)

{{ I and cond }}

S2 {{P2}}

{{ I and not cond }}

S3

{{P3}}

{{ Q }}

​

Loop Invariant

Consider a while-loop (other loop forms not too different)�with a loop invariant I. Let’s try forward reasoning...

​

Informally, we need:

• I holds initially
• I holds each time around
• Q holds after we exit

Formally, we need validity of:

• {{ P }} S1 {{ I }}
• {{ I and cond }} S2 {{ I }}
• {{ I and not cond }} S3 {{ Q }}

(can check these with backward reasoning instead)

​

​

​

16

{{ P }}

S1

{{P1}}

{{ Inv: I }}

while (cond)

{{ I and cond }}

S2 {{P2}}

{{ I and not cond }}

S3

{{P3}}

{{ Q }}

​

More on Loop Invariants

• Loop invariants are crucial information
• needs to be provided before reasoning is “turn the crank”

​

• Pro Tip: always document your invariants for non-trivial loops
• don’t make code reviewers guess the invariant

​

• Pro Tip: with a good loop invariant, the code is easy to write
• all the creativity can be saved for finding the invariant
• more on this in later lectures…

​

​

17

More on Loop Invariants

• Loop invariants are crucial information
• needs to be provided before reasoning is “turn the crank”

​

• Pro Tip: always document your invariants for non-trivial loops
• don’t make code reviewers guess the invariant

​

• Pro Tip: with a good loop invariant, the code is easy to write
• all the creativity can be saved for finding the invariant
• more on this in later lectures…

​

​

18

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

19

{{ }}

s = 0;

i = 0;

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

Equivalent to this “for” loop:

​

s = 0;

for (int i = 0; i != n; i++) {

s = s + b[i];

}

​

​

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

20

{{ }}

s = 0;

i = 0;

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

21

{{ }}

s = 0;

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

22

{{ }}

s = 0;

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

(s = 0 and i = 0) implies

s = b[0] + … + b[i-1] ?

​

Yes. (An empty sum is zero.)

​

​

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

23

{{ }}

s = 0;

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

• (s = 0 and i = 0) implies I�

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

24

{{ }}

s = 0;

i = 0;

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {� {{ s = b[0] + ... + b[i-1] and i != n }}

s = s + b[i];

i = i + 1;

{{ s = b[0] + ... + b[i-1] }}

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

• (s = 0 and i = 0) implies I�
• {{ I and i != n }} S {{ I }} ?

​

{{ s + b[i] = b[0] + … + b[i] }}

{{ s = b[0] + … + b[i] }}

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

25

{{ }}

s = 0;

i = 0;

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

• (s = 0 and i = 0) implies I�
• {{ I and i != n }} S {{ I }}�
• {{ I and not (i != n) }} implies

s = b[0] + … + b[n-1] ?

​

Example: sum of array

Consider the following code to compute b[0] + … + b[n-1]:

26

{{ }}

s = 0;

i = 0;

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

s = s + b[i];

i = i + 1;

}

{{ s = b[0] + ... + b[n-1] }}

​

​

​

• (s = 0 and i = 0) implies I�
• {{ I and i != n }} S {{ I }}�

{{ I and i = n }} implies Q

​

These three checks verify

the postcondition holds

(i.e., the code is correct)

​

​

​

Termination

• Technically, this analysis does not check that the code terminates
• it shows that the postcondition holds if the loop exits
• but we never showed that the loop actually exits
• However, that follows from an analysis of the running time
• e.g., if the code runs in O(n²) time, then it terminates
• an infinite loop would be O(∞)
• any finite bound on the running time proves it terminates
• It is normal to also analyze the running time of code we write, so we get termination already from that analysis.

27

Example HW Problem

28

Example HW Problem

The following code to compute b[0] + … + b[n-1]:

​

{{ }}

s = 0;

{{ ____________ }}

i = 0;

{{ ____________ }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ ____________ }}

s = s + b[i];

{{ ____________ }}

i = i + 1;

{{ ____________ }}

}

{{ ____________ }}

{{ s = b[0] + ... + b[n-1] }}

29

Example HW Problem

The following code to compute b[0] + … + b[n-1]:

​

{{ }}

s = 0;

{{ s = 0 }}

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ s = b[0] + … + b[i-1] and i != n }}

s = s + b[i];

{{ s = b[0] + … + b[i-1] + b[i] and i != n }}

i = i + 1;

{{ s = b[0] + … + b[i-2] + b[i-1] and i-1 != n }}

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

30

But are we done and is this ok?

Example HW Problem

We start by filling in the blanks, but we still need to check for more.

​

{{ }}

s = 0;

{{ s = 0 }}

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ s = b[0] + … + b[i-1] and i != n }}

s = s + b[i];

{{ s = b[0] + … + b[i-1] + b[i] and i != n }}

i = i + 1;

{{ s = b[0] + … + b[i-2] + b[i-1] and i-1 != n }}

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

31

Example HW Problem

Does the invariant hold initially (before the loop starts)?

​

{{ }}

s = 0;

{{ s = 0 }}

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ s = b[0] + … + b[i-1] and i != n }}

s = s + b[i];

{{ s = b[0] + … + b[i-1] + b[i] and i != n }}

i = i + 1;

{{ s = b[0] + … + b[i-2] + b[i-1] and i-1 != n }}

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

32

Yes, i = 0 implies that s = (b[0] + … + b[-1]) = 0.

Example HW Problem

Does the postcondition hold after the loop terminates?

​

{{ }}

s = 0;

{{ s = 0 }}

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ s = b[0] + … + b[i-1] and i != n }}

s = s + b[i];

{{ s = b[0] + … + b[i-1] + b[i] and i != n }}

i = i + 1;

{{ s = b[0] + … + b[i-2] + b[i-1] and i-1 != n }}

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

33

Yes, not (i != n) implies i = n,

thus s = b[0] + ... + b[n-1].

Example HW Problem

Does the loop body preserve our invariant?

​

{{ }}

s = 0;

{{ s = 0 }}

i = 0;

{{ s = 0 and i = 0 }}

{{ Inv: s = b[0] + ... + b[i-1] }}

while (i != n) {

{{ s = b[0] + … + b[i-1] and i != n }}

s = s + b[i];

{{ s = b[0] + … + b[i-1] + b[i] and i != n }}

i = i + 1;

{{ s = b[0] + … + b[i-2] + b[i-1] and i-1 != n }}

}

{{ s = b[0] + ... + b[i-1] and not (i != n) }}

{{ s = b[0] + ... + b[n-1] }}

34

Yes, weaken by dropping i-1 != n.

Yes, equivalent to (Inv and loop condition).

HTML

35

HTML, Formally

• Hyper-Text Markup Language�
• Consists tags and their content
• components become tags
• input fields, buttons, etc.
• containers have start and end tags
• tags placed in between are children
• additional information provided to the tag with “attributes”

​

36

Anatomy of a Tag

Element�

<p> Some Text </p>

​

Tag Name Content Closing Tag

37

Anatomy of a Tag

Element�

<p id=”firstParagraph”> Some Text </p>

​

Tag Name Content Closing Tag

Attribute Name Attribute Value

38

Tags form a Tree

<div>

<p id=”firstParagraph”> Some Text </p>

<br>

<div>

<p>Hello</p>

</div>

</div>

​

This tree, as it lives in the browser, is often called the "DOM"

– Document Object Model

​

​

39

Tags form a Tree

<div>

<p id=”firstParagraph”> Some Text </p>

<br>

<div>

<p><a href=”mypage.html”>Go to my page</a></p>

</div>

</div>

​

This tree, as it lives in the browser, is often called the "DOM"

– Document Object Model

​

​

40

div

p

br

div

p

a

Tags form a Tree

• See the W3Schools HTML reference for a complete list, along with all their supported attributes.
• Some worth knowing:
• <a> - defines a hyperlink used to link from one page to another.
• <p> - Paragraph tag, surrounds text with whitespace/line breaks.
• <div> - “The curly braces of HTML” - used for grouping other tags. Surrounds its content with whitespace/line breaks.
• <span> - Like <div>, but no whitespace/line breaks.
• <br /> - Forces a new line (like “\n”). Has no content.
• <html> and <head> and <body> - Used to organize

a basic HTML document.

41