c - boolean 抽象 C 程序

Question

我正在尝试使用谓词计算以下 C 代码片段的抽象:b: { x >= 0 }

1. if( x > 5 )
2.   x = x - 2;
3. else
4.   x = abs( x ) + 6;
5. assert( x >= 0 );

到目前为止我抽象了:

1. if( * ) // not sure if I should put if( b ) here
2.   assume( b ); b = true;
3. else
4.   assume( true ); // ? don't know how to abstract further
5. assert( b )

有什么想法可以做到这一点吗？

Answer 1

我不知道我的理解是否正确，但对于输入谓词集 {x>=0} 或 b (交替使用)。应该是:-

{x>=0}=unknown()   //unknown function is used to generate true or false non-deterministically

if(*)
{
 assume({x>=0});
 {x>=0}=true;
}
else
{
 assume(!{x>=0});
 {x>=0}=false;
}