c - ブール抽象化 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;
}