[Question][Hw4] How the filter works?

[ehdkacjswo]

Name: Doam Lee

I've read the README.md of hw4, and couldn't understand how the filter works. It says "filter pred v1 v2 will return a sound refinement of abstract numerical value v1 with respect to predicate pred and abstract numerical value v2". And for example, it argues that filter < [1, 10] [3, 5] will soundly refine the left interval to [1, 4], but filter <= [1, 10] [1, 10] will return [1, 10] because no refinement is possible. But since it has to be sound, the refined intervals shouldn't be [1, 2] and [1]? I'm not sure how it works.

[goodtaeeun]

We should consider all possibilities when we want soundness. Having an interval [1,10] means that any value from 1 to 10 is possible and an interval [3,5] means that any value from 3 to 5 is possible Then. when considering all possible cases of [1,10] < [3,5], [1,4] will be the resulting interval. The smallest possible value is 1 because it is the lower bound of the left-hand side of the comparison. The largest possible value is 4 because it is the largest value that is smaller than the upper bound of the right-hand side of the comparison. Combining these two, we get [1,4]

[ehdkacjswo]

Oh, it seems that I confused soundess with completness. It's not an important question, but on second case what does "No refinement is possible" means? Does it means it still remains same after refinement?

[goodtaeeun]

Yes. the resulting interval of filter <= [1, 10] [1, 10] is still [1,10]. Thus, no refinement was made here.

[ehdkacjswo]

Thanks for your replies!