[Question][Hw5] About Instruction 3

[kws1207]

I can't understand the sentence (maybe because of my poor english):

• "Semantic function filter neg cond memory will return an abstract memory that soundly subsumes all possible concrete memories satisfiying condition cond (if neg is true, then the negation of cond)."

, especially the part inside the parenthesis.

Can someone please explain more clearly, maybe with some examples?

[RiceBiscuits]

It seems that the instruction 2 has more detail explanation.

You will define the filter function for memories (Semantics.Make.filter) using the ones for values. The first argument of the function represents whether the condition (i.e., the second argument) is true or not. For example, filter (x < 10) true mem will return an abstract memory that satisfies condition x < 10. On the other hand, filter (x < 10) false mem will return an abstract memory that does not satisfy condition x < 10.

[kws1207]

Thanks