For each of the two code samples shown, use the weakest precondition approach to derive any necessary precondition in order to prove that the code is partially correct with respect to the specification. Sample $2$ uses information derived from the tokeneer scenario

Be sure to show each step in the derivation and indicate which proof rules have been used.

$1)$ Sums method

method Sums$($x: int, y: int$)$ returns $($m: int, n: int$)$

ensures m $>$ n

$\{$

var a: int;

m :$=$ x;

n :$=$ y;

a :$=2*$ m $+$ n;

n :$=$ n $-1$;

m :$=$ a;

$\}$

$2)$ Update Alarms method

datatype ALARM $=$ silent $|$ alarming

method UpdateAlarms$($doorAlarm: ALARM, auditAlarm: ALARM$)$ returns $($alarm: ALARM$)$

ensures $($alarm $==$ alarming$)<==>$

$($doorAlarm $==$ alarming$)||($auditAlarm $==$ alarming$)$

$\{$

if doorAlarm $==$ alarming $||$ auditAlarm $==$ alarming

$\{$ alarm :$=$ alarming; $\}$

else

$\{$ alarm :$=$ silent ;$\}$

$\}$