This is a course page of David Casperson |
|
Pending homework questions can be found at
http://casper.unbc.ca/Semesters/2019-05F/320-homework-pending.php
.
{P}if e then s1 else s2 endif
{Q} ?
To write the answer to this question, it is appropriate, and
probably necessary, to write things something like
“Suppose that P1 is the weakest
pre-condition such that
{P1}s1
{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
fall-2024