1
$\begingroup$

I was wondering about following. I have condition in my program that I want to prove its correctness (I won't write the whole problem, just the part I'm curious about):

  • if $w \leq r$ then $r:=r-w$;

What I'm trying to do is form loop invariant and I have the following problem (might sound silly but I'm clueless as of what to write).

$r_{j+1}= r_{j} + w_j \times {condition}$

I want to find a condition that holds following stuff: if $w\leq r$ return $1$ else return $0$ so I could just put it mathematically in $r_{j+1}$ above so it holds. I have no clue which expression should I form that gives $1$ if $w \leq r$ else $0$. I would be grateful if someone could help me.

$\endgroup$

1 Answer 1

1
$\begingroup$

You can always explicitly define such a function.

$f(x,y) = \begin{cases} 1, \quad x \leq y\\ 0, \quad otherwise\\\end{cases}$

And yes, this is a well defined function and such functions are very often used in mathematics, so you don't have to worry.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.