InforLorV4, PascalFrancis, Corpus, bibRecord, 000C04

Observational proofs with critical contexts

Identifieur interne : 000C04 ( PascalFrancis/Corpus ); précédent : 000C03; suivant : 000C05

Observational proofs with critical contexts

Auteurs : N. Berregeb ; A. Bouhoula ; M. Rusinowitch

Source :

Lecture notes in computer science [ 0302-9743 ] ; 1998.

RBID : Pascal:98-0233935

Descripteurs français

Pascal (Inist)
- Informatique théorique, Théorie programmation, Système réécriture, Spécification algébrique.

English descriptors

KwdEn :
- Algebraic specification, Computer theory, Programming theory, Rewriting systems.

Abstract

Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0302-9743`
A05				`@2 1382`
A08	`01`	`1`	`ENG`	`@1 Observational proofs with critical contexts`
A09	`01`	`1`	`ENG`	`@1 FASE'98 : fundamental approaches to software engineering : Lisbon, March 28 - April 4, 1998`
A11	`01`	`1`		`@1 BERREGEB (N.)`
A11	`02`	`1`		`@1 BOUHOULA (A.)`
A11	`03`	`1`		`@1 RUSINOWITCH (M.)`
A12	`01`	`1`		`@1 ASTESIANO (Egidio) @9 ed.`
A14	`01`			`@1 LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101 @2 54602 Villers-lès-Nancy Cedex @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut.`
A20				`@1 38-53`
A21				`@1 1998`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-64303-6`
A43	`01`			`@1 INIST @2 16343 @5 354000078902140030`
A44				`@0 0000 @1 © 1998 INIST-CNRS. All rights reserved.`
A45				`@0 18 ref.`
A47	`01`	`1`		`@0 98-0233935`
A60				`@1 P @2 C`
A61				`@0 A`
A64		`1`		`@0 Lecture notes in computer science`
A66	`01`			`@0 DEU`
A66	`02`			`@0 USA`
C01	`01`		`ENG`	@0 Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.
C02	`01`	`X`		`@0 001D02A07`
C03	`01`	`X`	`FRE`	`@0 Informatique théorique @5 01`
C03	`01`	`X`	`ENG`	`@0 Computer theory @5 01`
C03	`01`	`X`	`SPA`	`@0 Informática teórica @5 01`
C03	`02`	`1`	`FRE`	`@0 Théorie programmation @5 02`
C03	`02`	`1`	`ENG`	`@0 Programming theory @5 02`
C03	`03`	`3`	`FRE`	`@0 Système réécriture @5 03`
C03	`03`	`3`	`ENG`	`@0 Rewriting systems @5 03`
C03	`04`	`3`	`FRE`	`@0 Spécification algébrique @5 04`
C03	`04`	`3`	`ENG`	`@0 Algebraic specification @5 04`
N21				`@1 153`

A30	`01`	`1`	`ENG`	`@1 Fundamental approaches to software engineering. International conference @2 1 @3 Lisbon PRT @4 1998-03-28`

Format Inist (serveur)

NO :	PASCAL 98-0233935 INIST
ET :	Observational proofs with critical contexts
AU :	BERREGEB (N.); BOUHOULA (A.); RUSINOWITCH (M.); ASTESIANO (Egidio)
AF :	LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101/54602 Villers-lès-Nancy Cedex/France (1 aut., 2 aut., 3 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1998; Vol. 1382; Pp. 38-53; Bibl. 18 ref.
LA :	Anglais
EA :	Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.
CC :	001D02A07
FD :	Informatique théorique; Théorie programmation; Système réécriture; Spécification algébrique
ED :	Computer theory; Programming theory; Rewriting systems; Algebraic specification
SD :	Informática teórica
LO :	INIST-16343.354000078902140030
ID :	98-0233935

Links to Exploration step

Pascal:98-0233935

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Observational proofs with critical contexts</title>
<author><name sortKey="Berregeb, N" sort="Berregeb, N" uniqKey="Berregeb N" first="N." last="Berregeb">N. Berregeb</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Bouhoula, A" sort="Bouhoula, A" uniqKey="Bouhoula A" first="A." last="Bouhoula">A. Bouhoula</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, M" sort="Rusinowitch, M" uniqKey="Rusinowitch M" first="M." last="Rusinowitch">M. Rusinowitch</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">98-0233935</idno>
<date when="1998">1998</date>
<idno type="stanalyst">PASCAL 98-0233935 INIST</idno>
<idno type="RBID">Pascal:98-0233935</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C04</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Observational proofs with critical contexts</title>
<author><name sortKey="Berregeb, N" sort="Berregeb, N" uniqKey="Berregeb N" first="N." last="Berregeb">N. Berregeb</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Bouhoula, A" sort="Bouhoula, A" uniqKey="Bouhoula A" first="A." last="Bouhoula">A. Bouhoula</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, M" sort="Rusinowitch, M" uniqKey="Rusinowitch M" first="M." last="Rusinowitch">M. Rusinowitch</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="1998">1998</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algebraic specification</term>
<term>Computer theory</term>
<term>Programming theory</term>
<term>Rewriting systems</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Théorie programmation</term>
<term>Système réécriture</term>
<term>Spécification algébrique</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>1382</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Observational proofs with critical contexts</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>FASE'98 : fundamental approaches to software engineering : Lisbon, March 28 - April 4, 1998</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>BERREGEB (N.)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>BOUHOULA (A.)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>RUSINOWITCH (M.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>ASTESIANO (Egidio)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101</s1>
<s2>54602 Villers-lès-Nancy Cedex</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14>
<fA20><s1>38-53</s1>
</fA20>
<fA21><s1>1998</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-64303-6</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000078902140030</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 1998 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>18 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>98-0233935</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fA66 i1="02"><s0>USA</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02A07</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="1" l="FRE"><s0>Théorie programmation</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="1" l="ENG"><s0>Programming theory</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="3" l="FRE"><s0>Système réécriture</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="3" l="ENG"><s0>Rewriting systems</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="3" l="FRE"><s0>Spécification algébrique</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="3" l="ENG"><s0>Algebraic specification</s0>
<s5>04</s5>
</fC03>
<fN21><s1>153</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>Fundamental approaches to software engineering. International conference</s1>
<s2>1</s2>
<s3>Lisbon PRT</s3>
<s4>1998-03-28</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 98-0233935 INIST</NO>
<ET>Observational proofs with critical contexts</ET>
<AU>BERREGEB (N.); BOUHOULA (A.); RUSINOWITCH (M.); ASTESIANO (Egidio)</AU>
<AF>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique - B.P. 101/54602 Villers-lès-Nancy Cedex/France (1 aut., 2 aut., 3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1998; Vol. 1382; Pp. 38-53; Bibl. 18 ref.</SO>
<LA>Anglais</LA>
<EA>Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.</EA>
<CC>001D02A07</CC>
<FD>Informatique théorique; Théorie programmation; Système réécriture; Spécification algébrique</FD>
<ED>Computer theory; Programming theory; Rewriting systems; Algebraic specification</ED>
<SD>Informática teórica</SD>
<LO>INIST-16343.354000078902140030</LO>
<ID>98-0233935</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C04 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000C04 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:98-0233935
   |texte=   Observational proofs with critical contexts
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Observational proofs with critical contexts

Observational proofs with critical contexts

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri