Example with more-formal Logic
lA searching program:
lInput assertion:
la == a0
lOutput assertion:
la == a0 and
l(($i) a[i] == v) ¨ a[m] == v, and
l(("i) a[i] != v) ¨ m == -1