河野真治 @ 琉球大学情報工学です。

In article <YAS.04Sep10200724@kirk.is.tsukuba.ac.jp>, yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes
> 検証と２重チェックか。違いがよくわかりません。
> コンパイル時だと検証で、実行時だとチェックですか。

あらゆる可能な実行の可能性に対してチェックするのが検証です。
validity とか satisfiablity とか言う奴。( だから、その程度の
論理学は知らないと...)

assert は、特定の実行に対するチェックなので検証ではない。
もっとも、世の中の人はシミュレーションとかを検証とかいう
人もいるんですけどね。

コンパイル時の型チェックなどは、可能な実行状態に作用されない
ので、検証と同等になります。

> この時点であいまいだけど、たとえば、１秒としましょう。
>    ボタンを押すと、１秒以内に何らかの反応がある

「反応がある」っていうのを定義して、それに対してチェック
するみたいな感じ。

例えば、反応があったら特定の変数をセットするような感じ
にして、
     [] (ボタンが押される -> <> 反応変数がセット)
     常に                    いつか
みたいなのを検証します。あらゆるボタンの押す順序に対して。

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科