Class Math220

References:

State: a list of variables and there values.

Textual substitution

(x + 2y) [x,y := y,x]

is not the same as

(x + 2y) [x := y] [y := x]

==> the property of textual substitution.

Example:

((a + b) x ) [b:=x] [x:=b]

==> (a + b) b

((a + b) c) [b:=x] [x:=b]

==> (a + b) c

—> Provisal (provided that…)

$ If \not occurs ( ‘x’, ‘E’ )$, then

$ E[y:=x][x:=y] = E $

– a property of textual substitution.

Inference rule

  • a horizontal line
    • premise or hypothesis above the the line.
    • conclusion below the line.
  • The premise is assumed to be true in all states.

Example:

$2x = 10$ / $x = 5$

Equality

four laws/properties of equality: R S T L.

  • Reflexitivity: x = x.
  • Symmetry: (x=y) = (y=x) ; also known as ‘commutative’ law.
  • Transitivity: (X=Y, Y=Z) / (X=Z) ;
  • Leibniz. (X=Y) / (E(z:=X) = E(z:=Y))

Function Evaluation

A function is a rule for computing a value from another value.

Use dot . as function application g.z, in place of parenthesis: g(z).

g(z) = 2*x + 6

g.z : 2*x + 6

. (function application)

g(2 + 3)

g.2 + 3

Function evaluation is based on textual substitution. Always do the t.s. simultaneously.

Assignment Statement

Textual substitution: :=.

Uses the same symbol as text substitution.

y:= y+1

Math/formal methods c++ Java Python
:= =
= ==

Hoare Tripple


{P} S {Q}

P: precondition
S: statement
Q: postcondition

Assignment

Definition of assignment.


{ R [ x := E]} x:=E {R}

x := E : assignment statement, ":=" means "gets", to be executed.

R[x:=E] : textual substitution. ":=" means "replaced by". The precondition is calculated from the postcondition.

Calculate the precondition from the postcondition:

{??} x:=x+1 {x>4} –> {x + 1 > 4} x:=x+1 {x>4} –> {x > 3} x:=x+1 {x>4}

{??} y:=6 {x*y > 0} –> {x*6 > 0} y:=6 {x*y > 0} –> …

{??} x:=x*2 { x=10 } –> {x*2 = 10} x:=x*2 {x=10} –> …

{??} x:=y { y=6 } –> {y=6} x:=y {y=6} –> …

Definition of multiple assignments:

x,y := y,x  // Python: `x,y = y,x`

Hoare Triples for multiple assignments:

{y > x} x,y := y,x {x > y}

{x + i = 1 + 2 + ... + (i + 1 - 1)} x,i := x + i, i + 1 {x = 1 + 2 + ... + (i - 1)}

{x + i = 1 + 2 + ... + (i + 1 - 1)} i,x := x + i, i + 1 {x = 1 + 2 + ... + (i - 1)}

Boolean Expressions

Expressions: constants + variables

Boolean expressions:

  • Constants: true/T, false/T
  • Unary operator: $\neg$
  • Binary operators:
    • $=$, equals, for booleans or numbers.
    • $\equiv$, equivales, for booleans only.
    • $\neq$,
    • $\not\equiv$
    • or
    • and,
    • => implies
    • <= follows from
    • nand, not and
    • nor, not or
  • Variables:

Truth Table

Satisfied

A boolean expression P is satisfied in a state, if

P is satisfiable, if

Predicate

A predicate is a function that returns type boolean.

Valid

Boolean expression P is valid if it is satisfied in every state.

Valid(P) is a predicate that returns true if P is a valid boolean expression and false otherwise.

dual

dual of a boolean expression P, $P_D$, is constructed from P by interchanging occurrences of

  • true and false,
  • $\wedge$ and $\vee$,
  • $\equiv$ and $\not \equiv$,
  • $\Rightarrow$ (implies) and $\nLeftarrow$ (not follow from),
  • $\Leftarrow$ (follow from) and $\not \Rightarrow$ (not implies).

P and $\neg P_D$ are not the same expression.

Metatheorem Duality

(2.3)

$valid(P) \equiv valid(\neg P_D) $

$valid(P\equiv Q) \equiv valid(P_D \equiv Q_D)$

Sufficient/Sufficiency and Necessary/Necessity

Equality vs. Equivalence

$=$ and $\equiv$ have the same truth table.

$=$ is for numbers or booleans.

$\equiv$ is only for booleans.

Three differences:

  • $=$ has higher precedence than $\equiv$.
    • Example: $x*y=0 \equiv x=0 \vee y=0$
  • $=$ is conjunctional while $\equiv$ is not.
    • Example: $b=c<d$ means $b=c \wedge c<d $
    • Example: $b=c=d$ means $b=c \wedge c=d $
  • $\equiv$ is associative while $=$ is not.
    • Example: suppose state (b, false) (c, false) (d, true)
    • $(b\equiv c) \equiv d$ is the same as:
    • $b \equiv (c\equiv d)$

Prove:

Since $=$ is conjunctional, it cannot be associative.

inside computer logic circuits, are $\vee, \wedge, \equiv$, … but mathematitions, do not use $\equiv$.

Propositional Calculus

Calculus: process of reasoning by manipulating(calculating with) symbols.

Propositional Calculus: a method of calculating with boolean expressions that involve propositional variables.

Symbols: conjunctions, disjunctions, implies. …

Proposition: a declarative sentence that is either true or false.

Axiom: a boolean expression that defines the properties of boolean operators.

Axioms are never proved. They are assumed to be valid.

Euclidean Geometry: 13 Euclidean /wukliam/ axioms.

Theorem: Either (1) an axiom or (2) a thorem that is proved equal to an axiom or a previously proved theorem.

Axiom, Associativity of $\equiv$: $((p \equiv q)\equiv r) \equiv (p \equiv (q \equiv r))$. (3.1)

Axiom, Symmetry of $\equiv$: $p\equiv q \equiv q \equiv$ p. (imagining as follows: $(p\equiv q) \equiv (q \equiv p )$). (3.2)

Axiom, Identity of $\equiv$: $true \equiv q \equiv q$. (3.3)

Exercise:

Prove: $p \equiv p \equiv q \equiv q$

Proof:

$ p \equiv p \equiv q \equiv q $

step1: apply 3.2 Aiom: $(p \equiv q \equiv q) \equiv p $, replace $(p \equiv q \equiv q)$ with p.

$ p \equiv p $

step2: replace first p by $(p \equiv q \equiv q)$

$p \equiv q \equiv q \equiv p $

apply 3.2. //

Latin: Q.E.D. it has been demostrated.

identity

Identity:

true is the identity of $\equiv$.

p = (true $\equiv$ p)

(p $\equiv$ true) = p.

Prove: true.

step1: apply 3.3. with $q\equiv true$

$true \equiv true \equiv true$ ==> $ true \equiv true$

step2: apply 3.3, replace 2nd true with $q \equiv q$

$true \equiv q \equiv q$

apply 3.3. //

Prove: $p \equiv p$

step1: apply 3.3. let p:=q

$true$.

step2: apply 3.4. //

More

Created Jan 19, 2023 // Last Updated Feb 22, 2023

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?