Formal derivation of spanning trees algorithms
Identifieur interne :
000701 ( PascalFrancis/Corpus );
précédent :
000700;
suivant :
000702
Formal derivation of spanning trees algorithms
Auteurs : Jean-Raymond Abrial ;
Dominique Cansell ;
Dominique MerySource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2003.
RBID : Pascal:04-0199981
Descripteurs français
English descriptors
Abstract
Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 2651 |
|---|
| A08 | 01 | 1 | ENG | @1 Formal derivation of spanning trees algorithms |
|---|
| A09 | 01 | 1 | ENG | @1 ZB 2003 : formal specification and development in Z and B : Turku, 4-6 June 2003 |
|---|
| A11 | 01 | 1 | | @1 ABRIAL (Jean-Raymond) |
|---|
| A11 | 02 | 1 | | @1 CANSELL (Dominique) |
|---|
| A11 | 03 | 1 | | @1 MERY (Dominique) |
|---|
| A12 | 01 | 1 | | @1 BERT (Didier) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 BOWEN (Jonathan P.) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 KING (Steve) @9 ed. |
|---|
| A12 | 04 | 1 | | @1 WALDEN (Marina) @9 ed. |
|---|
| A14 | 01 | | | @1 LORIA, Université Henri Poincaré Nancy 1 @3 FRA @Z 2 aut. |
|---|
| A14 | 02 | | | @1 LORIA, INRIA Lorraine, BP 239 @2 Vandeouvre-lès-Nancy @3 FRA @Z 3 aut. |
|---|
| A20 | | | | @1 457-476 |
|---|
| A21 | | | | @1 2003 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-40253-5 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000117777200260 |
|---|
| A44 | | | | @0 0000 @1 © 2004 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 21 ref. |
|---|
| A47 | 01 | 1 | | @0 04-0199981 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| C01 | 01 | | ENG | @0 Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook. |
|---|
| C02 | 01 | X | | @0 001D02B01 |
|---|
| C02 | 02 | X | | @0 001D02A02 |
|---|
| C03 | 01 | X | FRE | @0 Spécification formelle @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Formal specification @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Especificación formal @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Arbre maximal @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Spanning tree @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Arbol máximo @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Système réactif @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Reactive system @5 03 |
|---|
| C03 | 03 | X | SPA | @0 Sistema reactivo @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Méthode raffinement @5 16 |
|---|
| C03 | 04 | X | ENG | @0 Refinement method @5 16 |
|---|
| C03 | 04 | X | SPA | @0 Método afinamiento @5 16 |
|---|
| C03 | 05 | X | FRE | @0 Interprêtation abstraite @4 CD @5 96 |
|---|
| C03 | 05 | X | ENG | @0 Abstract interpretation @4 CD @5 96 |
|---|
| N21 | | | | @1 138 |
|---|
| N82 | | | | @1 PSI |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International conference of B and Z users @2 3 @3 Turku FIN @4 2003-06-04 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 04-0199981 INIST |
|---|
| ET : | Formal derivation of spanning trees algorithms |
|---|
| AU : | ABRIAL (Jean-Raymond); CANSELL (Dominique); MERY (Dominique); BERT (Didier); BOWEN (Jonathan P.); KING (Steve); WALDEN (Marina) |
|---|
| AF : | LORIA, Université Henri Poincaré Nancy 1 /France (2 aut.); LORIA, INRIA Lorraine, BP 239/Vandeouvre-lès-Nancy/France (3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2003; Vol. 2651; Pp. 457-476; Bibl. 21 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook. |
|---|
| CC : | 001D02B01; 001D02A02 |
|---|
| FD : | Spécification formelle; Arbre maximal; Système réactif; Méthode raffinement; Interprêtation abstraite |
|---|
| ED : | Formal specification; Spanning tree; Reactive system; Refinement method; Abstract interpretation |
|---|
| SD : | Especificación formal; Arbol máximo; Sistema reactivo; Método afinamiento |
|---|
| LO : | INIST-16343.354000117777200260 |
|---|
| ID : | 04-0199981 |
|---|
Links to Exploration step
Pascal:04-0199981
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Formal derivation of spanning trees algorithms</title>
<author><name sortKey="Abrial, Jean Raymond" sort="Abrial, Jean Raymond" uniqKey="Abrial J" first="Jean-Raymond" last="Abrial">Jean-Raymond Abrial</name>
</author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA, Université Henri Poincaré Nancy 1 </s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Mery</name>
<affiliation><inist:fA14 i1="02"><s1>LORIA, INRIA Lorraine, BP 239</s1>
<s2>Vandeouvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">04-0199981</idno>
<date when="2003">2003</date>
<idno type="stanalyst">PASCAL 04-0199981 INIST</idno>
<idno type="RBID">Pascal:04-0199981</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000701</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Formal derivation of spanning trees algorithms</title>
<author><name sortKey="Abrial, Jean Raymond" sort="Abrial, Jean Raymond" uniqKey="Abrial J" first="Jean-Raymond" last="Abrial">Jean-Raymond Abrial</name>
</author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA, Université Henri Poincaré Nancy 1 </s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Mery</name>
<affiliation><inist:fA14 i1="02"><s1>LORIA, INRIA Lorraine, BP 239</s1>
<s2>Vandeouvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2003">2003</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abstract interpretation</term>
<term>Formal specification</term>
<term>Reactive system</term>
<term>Refinement method</term>
<term>Spanning tree</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Spécification formelle</term>
<term>Arbre maximal</term>
<term>Système réactif</term>
<term>Méthode raffinement</term>
<term>Interprêtation abstraite</term>
</keywords><front><div type="abstract" xml:lang="en">Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>2651</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Formal derivation of spanning trees algorithms</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>ZB 2003 : formal specification and development in Z and B : Turku, 4-6 June 2003</s1>
</fA09><fA11 i1="01" i2="1"><s1>ABRIAL (Jean-Raymond)</s1>
</fA11><fA11 i1="02" i2="1"><s1>CANSELL (Dominique)</s1>
</fA11><fA11 i1="03" i2="1"><s1>MERY (Dominique)</s1>
</fA11><fA12 i1="01" i2="1"><s1>BERT (Didier)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>BOWEN (Jonathan P.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>KING (Steve)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="04" i2="1"><s1>WALDEN (Marina)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>LORIA, Université Henri Poincaré Nancy 1 </s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA14 i1="02"><s1>LORIA, INRIA Lorraine, BP 239</s1>
<s2>Vandeouvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>457-476</s1>
</fA20><fA21><s1>2003</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-40253-5</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000117777200260</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>21 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>04-0199981</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fC01 i1="01" l="ENG"><s0>Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02B01</s0>
</fC02><fC02 i1="02" i2="X"><s0>001D02A02</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Spécification formelle</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Formal specification</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Especificación formal</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Arbre maximal</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Spanning tree</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Arbol máximo</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Système réactif</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Reactive system</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Sistema reactivo</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Méthode raffinement</s0>
<s5>16</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Refinement method</s0>
<s5>16</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Método afinamiento</s0>
<s5>16</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Interprêtation abstraite</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Abstract interpretation</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fN21><s1>138</s1>
</fN21><fN82><s1>PSI</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference of B and Z users</s1>
<s2>3</s2>
<s3>Turku FIN</s3>
<s4>2003-06-04</s4>
</fA30><server><NO>PASCAL 04-0199981 INIST</NO>
<ET>Formal derivation of spanning trees algorithms</ET>
<AU>ABRIAL (Jean-Raymond); CANSELL (Dominique); MERY (Dominique); BERT (Didier); BOWEN (Jonathan P.); KING (Steve); WALDEN (Marina)</AU>
<AF>LORIA, Université Henri Poincaré Nancy 1 /France (2 aut.); LORIA, INRIA Lorraine, BP 239/Vandeouvre-lès-Nancy/France (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2003; Vol. 2651; Pp. 457-476; Bibl. 21 ref.</SO>
<LA>Anglais</LA>
<EA>Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.</EA>
<CC>001D02B01; 001D02A02</CC>
<FD>Spécification formelle; Arbre maximal; Système réactif; Méthode raffinement; Interprêtation abstraite</FD>
<ED>Formal specification; Spanning tree; Reactive system; Refinement method; Abstract interpretation</ED>
<SD>Especificación formal; Arbol máximo; Sistema reactivo; Método afinamiento</SD>
<LO>INIST-16343.354000117777200260</LO>
<ID>04-0199981</ID>
</server>
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 000701 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000701 | 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:04-0199981
|texte= Formal derivation of spanning trees algorithms
}}
| 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 |  |
