読者です 読者をやめる 読者になる 読者になる

PVSの使い方

今更ですが,使い方です.端末から

pvs

とすると,emacsが起動し

M-x nf

でNew file name:と尋ねられ,例えばdemoe20160519と適当に入力すれば,demo20160519.pvsが

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  

  END demo20160519

のような初期内容で生成されます.そこで,例えば

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
A:TYPE+
a:A
x,y:var A
p:[A->bool]
  % ENDASSUMING

f01:lemma exists(x):(p(x)=>(forall(y):(p(y))))
  

  END demo20160519

のように宣言とステートメントと書き込み(type,var,lemmaといった予約語case insensitive

M-x pr

とすれば

Installing rewrite rule sets.singleton_rew (all instances)


f01 :  

  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))

Rule? 

のような*pvs*バッファが開くので,以下のように順次入力する(実際には,TABの後に,fでflatten,iでinstなどのバインドを用います.キーバインド一覧はTAB h,また,コマンドの一覧はTABのみの連打,*pvs* への復帰はq)と

f01 :  

  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))

Rerunning step: (inst-cp 1 "a")
Instantiating (with copying) the top quantifier in 1 with the terms:
a,
this simplifies to: 
f01 :  

  |-------
[1]   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (p(a) => (FORALL (y): (p(y))))

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
f01 :  

{-1}  p(a)
  |-------
[1]   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (FORALL (y): (p(y)))

Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to: 
f01 :  

{-1}  p(a)
  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (p(y))

Rerunning step: (inst 1 "y")
Instantiating the top quantifier in 1 with the terms: 
 y,
this simplifies to: 
f01 :  

[-1]  p(a)
  |-------
{1}   (p(y) => (FORALL (y): (p(y))))
[2]   (p(y))

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
Q.E.D.

となり,先のバッファに戻るので,ポインターをf01上に置き

C-c 2 p

とすれば

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
A:TYPE+
a:A
x,y:var A
p:[A->bool]
  % ENDASSUMING

f01:lemma exists(x):(p(x)=>(forall(y):(p(y))))

%|- f01 : PROOF
%|- (then (inst-cp 1 "a") (flatten) (skeep*) (inst 1 "y") (flatten))
%|- QED
  

  END demo20160519

のようにプルーフスクリプトが書き込まれます.手を加えたい場合は,先度,M-x pr,もしくは直接

%|- f01 : PROOF
%|- (then (inst-cp + "a") (flatten) (skeep*) (inst + "y") (flatten))
%|- QED

のように書き換え,ポインタースクリプト上に置き

C-c ! p

とすれば,インストールされます.なお,コメントアウトには,C-c ; が使えます.

また,*pvs*上での一般の操作でよく用いるのは

クイットは,q,または,C-z z
(grindが帰ってこないときなどに便利な)インタラプトは,C-c C-c
で,LISPに入ってしまった場合の復帰は,(restore)
コマンドの前後に括弧を付して実行は,C-j
コマンド履歴は.M-s,または,C-上下矢印

辺りでしょう.