This is a course page of David Casperson 

Pending homework questions can be found at
http://casper.unbc.ca/Semesters/201905F/320homeworkpending.php
.
{P}if e then s_{1} else s_{2} endif
{Q} ?
To write the answer to this question, it is appropriate, and
probably necessary, to write things something like
“Suppose that P_{1} is the weakest
precondition such that
{P_{1}}s_{1}
{Q}
and that….”
NB The font may not be clear here. I am asking for partial correctness assertions, not total correctness assertions.
The code below gives a fragment of an algorithm to provide a candidate for a majority element.
If the algorithm works correctly, and data
has a
majority element, then candidate
will be equal to
that element at the end of the loop.
int count1 = 0 ; E candidate = null ; for (int i=0;i<data.length;++i) { if (count1==0) { candidate = data[i] ; count1=1; } else if (candidate.equals(data[i])) { count1 += 1 ; } else { count1 = 1 ; } }Attempt to find an axiomatic semantic proof of the correctness of this code.
E[e] : E → S → V
where
x++
and
++x
?
E[.x++
] and E[++x
]
let b in e
.
<expr> ::= <term>  <expr> + <term>  <expr>  <term> <term> ::= <factor>  <term> * <factor>  <term> / <factor> <factor> ::= ( expr )  number  variable
^
or **
) and unary minus.  x
x ^ y ^ z
 x ^ y
(and explain how you want this to group)x ^  y