Some problems about function summary

Shall I rephrase your ideas more formally:

Suppose under constaint C, the precise summary is S. But we could hardly get S usually. We could generate 3 kinds of summary:

S1: what must happens, i.e., S1 is contained by S.

S2: what could happen, but I know that nothing more can happen, i.e. S2 contains S.

S3: what could happen, but I don’t know if other can happen, i.e., the intersection of S3 and S is not empty, but no one contains another.