Program development by proof transformation [Elektronische Ressource] / vorgelegt von Luca Chiarabini

Luca Chiarabini And Philippe Audebaud

Sujets

• Mathematics

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2009
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Program
M?nc
Development
Transf
b
v
y
Development
Pro
LudwigMaximiliansUniv
of
v
T

ransfo
Pr
rmation
Pr

tion
Chia
ersit?t
rabini
hen
Dissertation
orgelegt
an
on
der
Chiarabini
F
Chiarabini
akult?t
ogram
f?r
by
Mathematik,
oof
Informatik
orma
und
Statistikter:
Dissertation
4.
an
3.
der
Ersatzpr?fer:
F
T
akult?t
Rolf
f?r
Hans
Mathematik,
Wirsing
Informatik
Berardi
und
b
Statistik
Prof.
der
k
Ludwig-Maximilians-Univ
Prof.
ersit?t
Ohlbac
M?nc
Dr.
hen

1.
Dr.

ersit?
h
ten
terstatter:
erg
Prof.
Pr?fer:
Dr.
Dr.
V
Hennic
olk
er
er
Pr?fer:
Heun
Dr.
2.
J?rgen

h
h
Prof.
terstatter:
Martin
Prof.
Externer
Dr.
h
Helm
Prof.
ut
Stefano
Sc
(Univ
h
di

orino)
hivun
With
not
all
e
its
(p
sinful
skies.
doings,
syllables
I
w
m
on
ust
e
sa
language,
y
if
,
gen
Con
e
tutti
scoppiettan
i
bronze,
suoi
grandi,
p
la

su
dev
Story
o
oi,
dire
il
That
Che
Italy's
South,
a
Le
pleasan
v
t
Come
place
sputter
for
to
me,

Che
And
l'Italia
o
mi
things
piace,
bro

a
he
lips,
mi
as
piace
il
Who
Lord
lo
Latin,
v
Whic
e
female
to
donna,
see
e
the
scritto
Sun
of
shine
ti
ev
all
ery
scorrono
da
t
y
to
,
whistling,
V
he,
edere
hiss,
il
hi
sole
e
splendere
m
ogni
donne,
giorno,

And

vines
ey
(not
v
nail'd
e
to
that
w
ti
alls)
o
from
holy
tree
But
to

tree
atico,
E
her
le

viti
sunn
non

pian
o:
tate
Storia
su
e
un
soft
m
lingua,
uro,
latino
F
melts
esto
from
on'd,
Morbido
m
di
uc
sounds
h
should
lik
on
e

the
raso,

h
k
sw
scene
e
of
mezzogiorno,
a
liquids
pla
pat
y

Ma
tili,
abbarbicate
single
ai


nessun
fondi
rozzo
Or
harsh
melo
ting
drame,
gutturali
whic
Whic
h
oblig's
p
spit,
eople
O
o
he

I
k
w
to
(forgiv
see
folly),
D'op
amo
era
rom
do
p
v
of
e

la
tadine
gen
blac
te
that

ou
When
E
the
hi
rst
ti,
act
ra
is
y
ended

b
tutto
y
te,
a
high
dance
more
Quando
Le
una
te
danza
and

and
hiude

il
sguardo
primo
on
atto,
soul
In
es,
viney
sugli
ards
l'anima,


from
as
the
e
south

of
Da
F
V
rance.
o:
T
℄
ra
v
vigne
the
rosseggian
that
ti
bastard

La
in
p
F
quel
rancia.
bastardo
I
h
also
lik
lik
kisses
e
a
to
mouth,
dine

on

b
una

And
Mi
as
piace
it
p
b
oi
writ
mangiare
satin,
b
vibra

se
hi,
sul
T
With
o
whic
see
breathe
the
the
Sun
eet
set,
Sillab
sure
respiran
he'll
il
rise
And
to-morro
tle
w,
gliding
Guardare
so
il
in,
sole
liquide

he
he
gen
tramon
That
ta,
a


Not
seems
through
Do
a
e
mist

y
suona
morning
Lik
t
our
winkling
northern
w
grun
eak
guttural,
as
le
Che
nordic
domani
grugniti
risorge
h
e
e're
non
to
opaco
and
A
and
drunk
all.
en

man's

dead
sputiamo,
ey
ti.
e
lik
in
the
maudlin
omens
sorro
o
w,
e
Come
y
un
Inne
o
erdonate)

le
hio
F
ubriaco
the
tra
h
le
easan
n
heek
ubi,
ruddy
But
Le
with
he
all

Hea
bronzee,
v
large
en
k
t'himself;
es
that
ash
da
y
y
a
will
olley
break
gli
as

Ma
neri,
in
irradian
pieno
e

Of
rinascer?
ys
il
sa
giorno,
thousand
Beauteous
at
as
Che


nor
in
b
istan
e
T
fore'd
the
to
dama's
b
w,
orro
melanc
w
,

dame,
te
fron
e
malinconica,
senza

n
with
uv
wild
ole,
liquid
e
Ma
non
hiara
gono
dallo
That
selv
sort
Heart
of
her
farthing
and

within
t
ey
whic
Cuore
h
labbra,
glimmers
o
Di
hi
quel
Soft
torv
her
o
and

y
di
her

Solare
When
dolce
reeking
il
London's
e
smoky


Bepp
simmers.
A
Del
enetian
fetido
[Bepp
b
Una
ollore
V
londinese.
di
I
Byron
lo
vvidem

on
In
Generierung
the
die
last
generation.
20
eines
y
die
ears
Ziel
the
essen
formal
Soft-

hen
h
den
to
y
the
ad
dev
ec
elopmen
eit
t
zu
of
has
soft
h
w
?u?erst
are
Grundlage
turned
formalen
out
hen
to
pro
b
F
e
h
a
erden

COQ,

erden.
hnique
Manipula-
for
gro?e
the
automatisc
generation
de
of
wird

y
programs.
also
This
20
idea
Metho
has

its
T

heraus.
base
auf
in
Um
to
das
the
hreibt,
sev
k.
eral
h
semi-automatic
ist,
metho
en
ds
x
to
ein
transform
in
a
erf?llt
formal
w
sp
o

A
that
ts
describ

e
etabliert
the
Bew
b
zu
eha
gefunden.
vior
v
of
he
a

program
onstruktiv
in
w
to
pro
an
studied
eectiv
of
e
big
executable

piece
den
of
stellte

Einsatz
de.
in
One
areen
of
als
this
h
is
hnik
the
orrekter
so-called
theoretisc
"program
Idee
extraction
semiautomatis-
from
den
pro
andlung
of".
ezizierung,
The
erhal-
idea
b
is
einem
that
deblo
from
dieser
an
t

extraction
e
Die
pro
wir
of
k
of
eis
a
f?r
form
istiert
ula
dass
"for
t

k
h

x
haft
there
Heutzutage
exists
he
y
v


h
erzeugt
that
MINLOG,
P(x,y)"
A,
w
of
e
t

w

diese
extract
heutzutage
a
hat
program
v
"t"
mit

te
h
k
that
h
the
dieser
prop
erden
ert
sc
y
und
P(x,t(x))
den
hold.
en
In
eln,
our
on
da
Bew
ys
Unser


h
Bioinformatik
pro
ofs,
ofs
tially
are
b
normally
pro
written
theorist,
b
a
y
eect
ad-ho
in

program
to
In
ols
letzten
(some
Jahren
of

them
der
are:
formaler
COQ,
den
ISABLLE,
der
MINLOG,
w
PX,
t
A
klung
GD
eine
A,


tige

ec
"pro
zur
of
k
assistan
Programmen
ts".
Die
Ev
he
en