Precondition of while loop program

K

kan

New member
Joined
May 28, 2020
Messages
14
I am having trouble finding precondition for the following program. Consider the following program segment:
Code: 
x:=x+y;
if (x<0) then
   abort
else
   while (x != y) do
     x:=x+1;
     y:=y+1
   od
fi

If it is assumed that its postcondition is [MATH]x=y[/MATH], then which condition is its precondition?

Hope for the help of everyone. Thanks for very much!
 
kan said:
I am having trouble finding precondition for the following program. Consider the following program segment:
Code: 
x:=x+y;
if (x<0) then
   abort
else
   while (x != y) do
     x:=x+1;
     y:=y+1
   od
fi

If it is assumed that its postcondition is [MATH]x=y[/MATH], then which condition is its precondition?

Hope for the help of everyone. Thanks for very much!
Click to expand...
Nice infinite loop. What's the point of this program?
You need to look up definitions of the 2 terms.
 
HallsofIvy said:
The precondition is \(\displaystyle x\ge 0\). Do you see why?
Click to expand...
I thinked the precondition is [MATH]x\geq 0[/MATH]. Because These are some of the choices that professors at my university make:
a) [MATH]x=2y[/MATH] and [MATH]y<2[/MATH]b) [MATH]x>2y[/MATH] and [MATH]y=2[/MATH]c) [MATH]x=2y[/MATH] and [MATH]y>2[/MATH]d) [MATH]x<2y[/MATH] and [MATH]y>2[/MATH]
 
Please show us the entire problem as given to you, including choices, and all typed correctly, so we can be sure what we're dealing with. Having pieces added and corrected bit by bit gets confusing.
 
The precondition is \(\displaystyle x\ge 0\) because the condition "if (x< 0) then abort" comes before the loop and means that x must be greater than or equal to 0 in order that the routine not abort and the loop runs.
 
Dr.Peterson said:
Please show us the entire problem as given to you, including choices, and all typed correctly, so we can be sure what we're dealing with. Having pieces added and corrected bit by bit gets confusing.
Click to expand...
The problem has been fully presented, looking forward to the help!
 
HallsofIvy said:
The precondition is \(\displaystyle x\ge 0\) because the condition "if (x< 0) then abort" comes before the loop and means that x must be greater than or equal to 0 in order that the routine not abort and the loop runs.
Click to expand...
Sorry, but it is not in what I selected
 
The loop continues while x != y. I'm _guessing_ the post-condition has to do with program's termination. Since initially x is incremented by y and then at every iteration y is incremented by 2 and x by 1, there is a specific condition for when x and y become equal and the program terminates.
 
I guess I have to put it together myself in order to make it easier to follow. Apparently the problem was this:

Consider the following program segment:
Code: 
x:=x+y;
if (x<0) then
   abort
else
   while (x != y) do
     x:=x+1;
     y:=y+2
   od
fi

If it is assumed that its postcondition is [MATH]x=y[/MATH], then which condition is its precondition?

a) [MATH]x=2y[/MATH] and [MATH]y<2[/MATH]b) [MATH]x>2y[/MATH] and [MATH]y=2[/MATH]c) [MATH]x=2y[/MATH] and [MATH]y>2[/MATH]d) [MATH]x<2y[/MATH] and [MATH]y>2[/MATH]

Since you only said those were some of the choices, I'm not sure. Is this exactly what it said?

If this is asking which of the listed conditions must be true initially in order for the program to terminate, then I think the problem is bad. I seem to have proved that it will terminate whenever x is a non-negative integer.

You could try running the program with sets of inputs corresponding to the negation of the various choices and see whether it fails to terminate. For example, if I take x=4 and y=2, I have not satisfied (a) or (c), but it does terminate, so (a) and (c) can't be right. I believe you can similarly eliminate the other choices.

All that leaves, in my mind, besides a simply bad (or miscopied) problem, is that your definition of precondition may not be what I think it is. Can you quote the definition you were given? (I would have agreed with posts #3, 4, 7.)
 
Dr.Peterson said:
I guess I have to put it together myself in order to make it easier to follow. Apparently the problem was this:

Consider the following program segment:
Code: 
x:=x+y;
if (x<0) then
   abort
else
   while (x != y) do
     x:=x+1;
     y:=y+2
   od
fi

If it is assumed that its postcondition is [MATH]x=y[/MATH], then which condition is its precondition?

a) [MATH]x=2y[/MATH] and [MATH]y<2[/MATH]b) [MATH]x>2y[/MATH] and [MATH]y=2[/MATH]c) [MATH]x=2y[/MATH] and [MATH]y>2[/MATH]d) [MATH]x<2y[/MATH] and [MATH]y>2[/MATH]

Since you only said those were some of the choices, I'm not sure. Is this exactly what it said?

If this is asking which of the listed conditions must be true initially in order for the program to terminate, then I think the problem is bad. I seem to have proved that it will terminate whenever x is a non-negative integer.

You could try running the program with sets of inputs corresponding to the negation of the various choices and see whether it fails to terminate. For example, if I take x=4 and y=2, I have not satisfied (a) or (c), but it does terminate, so (a) and (c) can't be right. I believe you can similarly eliminate the other choices.

All that leaves, in my mind, besides a simply bad (or miscopied) problem, is that your definition of precondition may not be what I think it is. Can you quote the definition you were given? (I would have agreed with posts #3, 4, 7.)
Click to expand...
That's really what the multiple-choice test the professor asked us. I solved and only got the result [MATH]x\geq 0[/MATH]. But after searching the internet, I found the following document, can you explain how they do it, because it's really hard to understand if the question on my test can only

 
Please tell us the context of your problem. What have you been learning, and specifically, what definition were you given for precondition? Which of the concepts used in that paper (e.g. Hoare calculus, weakest precondition) have you heard of?
 
Dr.Peterson said:
Please tell us the context of your problem. What have you been learning, and specifically, what definition were you given for precondition? Which of the concepts used in that paper (e.g. Hoare calculus, weakest precondition) have you heard of?
Click to expand...
This is what I have learned
 

Attachments

  • Program Verification_Handout.pdf
    420.4 KB · Views: 3
TBH I didn't understand the pdf in post #14. But I'm pretty certain that the following TWO pre-conditions are correct (which don't match your multiple choice options). Read comments A, then B, then C...

Rich (BB code): 
# C) Here we want x+y >= y AND x+y>=0
#
#    This simplifies to x>=0 AND x>=-y (perhaps y can be -ve so both conditions are important)

x:=x+y;

# B) We want x>=y AND ALSO x>=0  (the latter is added because of the "if x<0 abort")

if (x<0) then
   abort
else
   # A) We want x>=y here otherwise the loop won't stop (at least until y overflows)
   while (x != y) do
     x:=x+1;
     y:=y+2
   od
fi
 
You must log in or register to reply here.
Top