tutorial

Informations

• Publié par: Vouv
• Nombre de lectures: 66
• Langue: Español

Extrait

N
parameterized
these
T
in
utorial
Sp
on
examples
Using
supp
PVS
.
for
Science
Hardw
p
are
e
V
as
eriation
rotot
?
tutorial
S
b
Owre
Computer
J
of
M
Owre
Rush
Lab
b
vided
y
con
,
pro
N
elined
Shank
hec
ar
1
and
of
M
v
K
In
Sriv
erience
as
Shank
f
L
o
Menlo
wre
Rush
rush
Man
b
P
y
b
,
System
shank
ark
ar
capabilities
sriv
and
as
e
g
are
slriom
w
Computer
w
Science
examples
Lab
has
oratory
for
,
the
SRI
an
In
PVS
ternational
eriation
Menlo
language
P
and
ark
to
CA
ted
94025
Theorem
USA
,
Abstract
man
PVS
1
stands
M
for
e
rotot
e
yp
,
e
F
V
Owre
eriation
The
System
R
It
ele
consists
SRI
of
ebruary
a
and
sp
Guide
eciation
and
language
ase
in
In
tegrated
1993.
with
w
supp
are
ort
y
to
ho
ols
can
and
in
a
of
theorem
eriation
pro
t
v
ed
er
of
PVS
hardw
tries
of
to
a
pro
cessor
vide
een
the
enc
mec
del
hanization
ers
needed
is
to
tation
apply
ripplearry
formal
tro
metho
stands
ds
e
b
It
oth
sp
rigorously
tegrated
and
to
pro
theorem
ductiv
PVS
ely
?
.
as
This
the
tutorial
Conference
serv
v
es
Design
to
and
in
Herrenalb
tro
,
duce
26-28,
PVS
Owre
and
and
its
b
use
PVS
in
atio
the
eta
con
ase
text
Lab
of
In
hard
ark
w
1993.
are
ar
v
J
eriation
y
In
Pr
the
cker
st
enc
section
eta
w
.
e
oratory
brie
ternational
sk
CA
etc
3
h
Shank
the
M
purp
.
oses
the
for
ci
whic
eri
h
R
PVS
Computer
is
,
in
Menlo
tended
F
and
and
the
o
rationale
erful
b
that
ehind
pro
its
b
design
PVS
men
demonstrate
tion
w
some
features
of
b
the
used
uses
the
that
text
w
hardw
e
v
and
W
others
presen
are
completely
making
ork
of
out
it
ofs
W
t
e
o
giv
are
e
One
an
the
o
is
v
pip
erview
micropro
of
that
the
b
PVS
used
sp
b
eciation
hmark
language
mo
and
c
pro
k
of
and
c
other
hec
a
k
implemen
er
of
The
Nit
PVS
adder
language
In
system
ducing
and
PVS
theorem
for
pro
yp
v
V
er
System
eac
consists
h
a
ha
eciation
v
in
e
with
their
ort
o
ols
wn
a
reference
pro
man
er
uals
tries
1
pro
;
This
2
w
;
presen
3
at
whic
Second
h
ternational
y
on
ou
Pro
will
ers
need
Circuit
to
Theory
study
Practice
in
Exp
order
Bad
to
Ger
mak
y
e
Septem
pro
er
ductiv
1994.
e
S
use
N
of
ar
the
J
sys
Rush
tem
y
A
The
p
Sp
o
ci
c
n
k
anguage
et
R
reference
le
card
.
summarizing
Science
all
oratory
the
SRI
features
ternational
of
P
the
CA
PVS
ebruary
language
2
system
Shank
and
S
pro
and
v
M
er
b
is
.
also
PVS
a
o
v
Che
ailable
A
The
efer
purp
e
ose
ual
of
R
this
ase
tutorial
Computer
is
Lab
not
,
to
In
describ
Menlo
e
ark
in
F
detail
1993.
the
S
features
N
of
ar
PVS
J
and
Rush
ho
y
w
User
to
for
use
PVS
the
e
system
ation
Rather
V
its
ation
purp
eta
ose
ele
is
.
to
Science
in
oratory
tro
SRI
duce
ternational
some
P
of
CA
the
ebruary
more
A
uniquew
ligh
a
the
w
mec
ers
hanization
Metho
needed
w
to
the
apply
are
formal
of
metho
y
ds
a
b
HDM
oth
b
rigorously
is
and
and
pro
W
ductiv
used
ely
in
.
er
The
y
sp
y
eciation
E
language
ecause
of
to
PVS
t
is
a
a
tain
higherrder
In
logic
features
with
in
a
pro
ric
the
h
out
t
pip
yp
capacit
e
size
system
w
and
as
is
circuits
quite
adder
expressiv
design
e
templating
w
vide
e
26],
ha
W
v
V
e
built
found
t
that
tec
most
hea
of
Another
the
should
mathematical
no
and
easy
computational
elopmen
concepts
tirely
w
ose
e
e
wish
ho
to
purp
describ
of
e
erful
can
PVS
b
b
e
hardw
form
completely
ulated
t
v
the
ery
that
directly
hmark
and
del
naturally
ted
in
is
PVS
ving
Its
see
theorem
through
pro
del
v
is
er
TPCD
or
of
pro
illustrates
of
Goals
c
as
hec
in
k
formal
er
examples
(w
elopmen
e
DM
use
[30],
either
[22,
term
call
though
yp
the
System
latter
w
is
as
more
w
correct
yp
is
ext
b
for
oth
our
in
w
teractiv
eriation
e
for
and
that
highly
e
mec
ailable
hanized
licenses
the
relativ
user
install
c
use
ho
of
oses
funded
eac
y
h
The
step
this
that
to
is
detail
to
PVS
b
to
e
Rather
applied
is
and
duce
PVS
more
p
o
erforms
that
it
b
displa
demonstrate
ys
features
the
used
result
text
and
v
then
presen
w
ork
aits
ofs
for
o
the
One
next
is
command
micropro
PVS
b
dirs
b
from
testing
most
of
other
hec
in
handle
teractiv
While
e
the
theorem
an
pro
theorem
v
w
ers
ted
in
the
the
ould
p
as
o
a
w
hec
er
second
of
of
its
as
basic
enc
steps
implemen
these
Nit
can
second
in
of
v
1.1
ok
PVS
e
PVS
decision
ed
pro
exp
cedures
or
for
applications
arithmetic
ds
and
the
equalit
e
y
Dev
,
t
a
dology
BDDased
[25,
prop
STP
ositional
and
sim
HDM
plir
27].
eien
e
t
PVS
hashingased
rotot
automatic
e
conditional
eriation
rewriting
b
induction
it
and
as
other
partly
relativ
a
ely
t
large
eigh
units
protot
of
e
deduction
explore
it
generation
dirs
hnology
from
E
other
,
highly
main
automated
vy
theorem
eigh
pro
v
v
system
ers
goal
in
PVS
b
as
eing
it
directly
b
con
freely
trolled
v
b
require
y
costly
the
and
user
e
W
ely
e
to
ha
main
v
and
e
Dev
b
t
een
PVS
able
as
to
en
p
b
erform
SRI
some
ternation