第9章で最弱事前条件の表記についていくつかの質問には例があります。 b ::= x | true | false
e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2
WP b P = P b
WP (let x = e1 in e2) P = WP e1 (fun x -> WP e2 P)
WP (ass
のvalとopaque型の構造体を前提としています。私はF *を初めて使用していますが、このチュートリアルはよく書かれていますが、参照できるようにいくつかの良いAPIページがありません。 だから私は、次の構成のための正確な意味を必要とする： assume val name: type
私はこの行は名前が使用されてソルバーに登録すると言うだろうか？ opaque type name (...)