2013-07-07から1日間の記事一覧

PVSのこと（11）

PVS にはカユイところに手が届く帰納法が色々と用意されています．例えば subrange_inductions[i: int, j: upfrom(i)]: THEORY BEGIN k: VAR subrange(i, j) p: VAR pred[subrange(i, j)] subrange_induction: LEMMA (p(i) AND (FORALL k: k < j AND p(k) IM…

PVSのこと（10）

うらなりに見える Yices ですが．．． http://d.hatena.ne.jp/ehito/searchdiary?word=%C3%E6%B4%D6%C3%CD の例です． lem1:lemma A(0)<x & (exists m:x<=A(m)) => (exists n:A(n)</x>