布尔抽象 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;
}