Formal Derivation of Spanning Trees Algorithms
Identifieur interne : 002633 ( Istex/Corpus ); précédent : 002632; suivant : 002634Formal Derivation of Spanning Trees Algorithms
Auteurs : Jean-Raymond Abrial ; Dominique Cansell ; Dominique MérySource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
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.
Url:
DOI: 10.1007/3-540-44880-2_27
Links to Exploration step
ISTEX:A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCBLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">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><affiliation><mods:affiliation>Marseille, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jr@abrial.org</mods:affiliation></affiliation></author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, Vandœuvre-lès-Nancy Cédex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Dominique.Mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>LORIA, INRIA Lorraine, BP 239, Vandœuvre-lès-Nancy Cédex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Dominique.Cansell@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCB</idno><date when="2003" year="2003">2003</date><idno type="doi">10.1007/3-540-44880-2_27</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002633</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002633</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">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><affiliation><mods:affiliation>Marseille, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jr@abrial.org</mods:affiliation></affiliation></author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, Vandœuvre-lès-Nancy Cédex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Dominique.Mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>LORIA, INRIA Lorraine, BP 239, Vandœuvre-lès-Nancy Cédex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Dominique.Cansell@loria.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Jean-Raymond Abrial</name><affiliations><json:string>Marseille, France</json:string><json:string>E-mail: jr@abrial.org</json:string></affiliations></json:item><json:item><name>Dominique Cansell</name><affiliations><json:string>LORIA, Université Henri Poincaré Nancy 1, BP 239, Vandœuvre-lès-Nancy Cédex, France</json:string><json:string>E-mail: Dominique.Mery@loria.fr</json:string></affiliations></json:item><json:item><name>Dominique Méry</name><affiliations><json:string>LORIA, INRIA Lorraine, BP 239, Vandœuvre-lès-Nancy Cédex, France</json:string><json:string>E-mail: Dominique.Cansell@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-6MRKL2RH-K</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>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.</abstract><qualityIndicators><score>8.056</score><pdfWordCount>6786</pdfWordCount><pdfCharCount>32522</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>20</pdfPageCount><pdfPageSize>430 x 650 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>88</abstractWordCount><abstractCharCount>605</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Formal Derivation of Spanning Trees Algorithms</title><chapterId><json:string>27</json:string><json:string>Chap27</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2003</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor></serie><host><title>ZB 2003: Formal Specification and Development in Z and B</title><language><json:string>unknown</json:string></language><copyrightDate>2003</copyrightDate><doi><json:string>10.1007/3-540-44880-2</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-44880-8</json:string></eisbn><bookId><json:string>3-540-44880-2</json:string></bookId><isbn><json:string>978-3-540-40253-4</json:string></isbn><volume>2651</volume><pages><first>457</first><last>476</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Didier Bert</name><affiliations><json:string>Laboratoire LSR-IMAG, CNRS, 681, rue de la Passerelle, BP 72, 38402, Saint-Martin-d’Heres Cedex, France</json:string><json:string>E-mail: Didier.Bert@imag.fr</json:string></affiliations></json:item><json:item><name>Jonathan P. Bowen</name><affiliations><json:string>CISM, London South Bank University, Borough Road, SE1 0AA, London, UK</json:string><json:string>E-mail: jonathan.bowen@sbu.ac.uk</json:string></affiliations></json:item><json:item><name>Steve King</name><affiliations><json:string>Department of Computer Science, University of York, YO10 5DD, Heslington, York, UK</json:string><json:string>E-mail: king@cs.york.ac.uk</json:string></affiliations></json:item><json:item><name>Marina Waldén</name><affiliations><json:string>Department of Computer Science, Åbo Akademi University, Lemminkäineng. 14 A, 20520, Turku, Finland</json:string><json:string>E-mail: marina.walden@abo.fi</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-6MRKL2RH-K</json:string></ark><publicationDate>2003</publicationDate><copyrightDate>2003</copyrightDate><doi><json:string>10.1007/3-540-44880-2_27</json:string></doi><id>A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCB</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Formal Derivation of Spanning Trees Algorithms</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2003">2003</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Formal Derivation of Spanning Trees Algorithms</title><author><persName><forename type="first">Jean-Raymond</forename><surname>Abrial</surname></persName><email>jr@abrial.org</email><affiliation><address><settlement>Marseille</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Dominique</forename><surname>Cansell</surname></persName><email>Dominique.Mery@loria.fr</email><affiliation><orgName type="institution">LORIA, Université Henri Poincaré Nancy 1</orgName><address><postBox>BP 239</postBox><settlement>Vandœuvre-lès-Nancy Cédex</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Dominique</forename><surname>Méry</surname></persName><email>Dominique.Cansell@loria.fr</email><affiliation><orgName type="institution">LORIA, INRIA Lorraine</orgName><address><postBox>BP 239</postBox><settlement>Vandœuvre-lès-Nancy Cédex</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCB</idno><idno type="ark">ark:/67375/HCB-6MRKL2RH-K</idno><idno type="DOI">10.1007/3-540-44880-2_27</idno></analytic><monogr><title level="m" type="main">ZB 2003: Formal Specification and Development in Z and B</title><title level="m" type="sub">Third International Conference of B and Z Users Turku, Finland, June 4–6, 2003 Proceedings</title><idno type="DOI">10.1007/3-540-44880-2</idno><idno type="book-id">3-540-44880-2</idno><idno type="ISBN">978-3-540-40253-4</idno><idno type="eISBN">978-3-540-44880-8</idno><idno type="chapter-id">Chap27</idno><editor><persName><forename type="first">Didier</forename><surname>Bert</surname></persName><email>Didier.Bert@imag.fr</email><affiliation><orgName type="department">Laboratoire LSR-IMAG</orgName><orgName type="institution">CNRS</orgName><address><street>681, rue de la Passerelle</street><postBox>BP 72</postBox><postCode>38402</postCode><settlement>Saint-Martin-d’Heres Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></editor><editor><persName><forename type="first">Jonathan</forename><forename type="first">P.</forename><surname>Bowen</surname></persName><email>jonathan.bowen@sbu.ac.uk</email><affiliation><orgName type="department">CISM</orgName><orgName type="institution">London South Bank University</orgName><address><street>Borough Road</street><settlement>London</settlement><postCode>SE1 0AA</postCode><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Steve</forename><surname>King</surname></persName><email>king@cs.york.ac.uk</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">University of York</orgName><address><settlement>Heslington, York</settlement><postCode>YO10 5DD</postCode><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Marina</forename><surname>Waldén</surname></persName><email>marina.walden@abo.fi</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">Åbo Akademi University</orgName><address><street>Lemminkäineng. 14 A</street><postCode>20520</postCode><settlement>Turku</settlement><country key="FI">FINLAND</country></address></affiliation></editor><imprint><biblScope unit="vol">2651</biblScope><biblScope unit="page" from="457">457</biblScope><biblScope unit="page" to="476">476</biblScope><biblScope unit="chapter-count">31</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation><orgName type="institution">Karlsruhe University</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName><affiliation><orgName type="institution">Utrecht University</orgName><address><country key=""></country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>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.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I14029</label><item><term type="Secondary" subtype="priority-1">Software Engineering</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-2">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-44880-2</BookID><BookTitle>ZB 2003: Formal Specification and Development in Z and B</BookTitle><BookSubTitle>Third International Conference of B and Z Users Turku, Finland, June 4–6, 2003 Proceedings</BookSubTitle><BookVolumeNumber>2651</BookVolumeNumber><BookSequenceNumber>2651</BookSequenceNumber><BookDOI>10.1007/3-540-44880-2</BookDOI><BookTitleID>77733</BookTitleID><BookPrintISBN>978-3-540-40253-4</BookPrintISBN><BookElectronicISBN>978-3-540-44880-8</BookElectronicISBN><BookChapterCount>31</BookChapterCount><BookHistory><OnlineDate><Year>2003</Year><Month>5</Month><Day>27</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2003</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I14029" Priority="1" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I1603X" Priority="2" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Didier</GivenName><FamilyName>Bert</FamilyName></EditorName><Contact><Email>Didier.Bert@imag.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Jonathan</GivenName><GivenName>P.</GivenName><FamilyName>Bowen</FamilyName></EditorName><Contact><Email>jonathan.bowen@sbu.ac.uk</Email></Contact></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>Steve</GivenName><FamilyName>King</FamilyName></EditorName><Contact><Email>king@cs.york.ac.uk</Email></Contact></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Marina</GivenName><FamilyName>Waldén</FamilyName></EditorName><Contact><Email>marina.walden@abo.fi</Email></Contact></Editor><Affiliation ID="Aff4"><OrgDivision>Laboratoire LSR-IMAG</OrgDivision><OrgName>CNRS</OrgName><OrgAddress><Street>681, rue de la Passerelle</Street><Postbox>BP 72</Postbox><Postcode>38402</Postcode><City>Saint-Martin-d’Heres Cedex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgDivision>CISM</OrgDivision><OrgName>London South Bank University</OrgName><OrgAddress><Street>Borough Road</Street><City>London</City><Postcode>SE1 0AA</Postcode><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>University of York</OrgName><OrgAddress><City>Heslington, York</City><Postcode>YO10 5DD</Postcode><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>Åbo Akademi University</OrgName><OrgAddress><Street>Lemminkäineng. 14 A</Street><Postcode>20520</Postcode><City>Turku</City><Country>Finland</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Chapter ID="Chap27" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>27</ChapterID><ChapterDOI>10.1007/3-540-44880-2_27</ChapterDOI><ChapterSequenceNumber>27</ChapterSequenceNumber><ChapterTitle Language="En">Formal Derivation of Spanning Trees Algorithms</ChapterTitle><ChapterFirstPage>457</ChapterFirstPage><ChapterLastPage>476</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2003</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2003</Year><Month>5</Month><Day>26</Day></RegistrationDate><OnlineDate><Year>2003</Year><Month>5</Month><Day>27</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>3-540-44880-2</BookID><BookTitle>ZB 2003: Formal Specification and Development in Z and B</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff8"><AuthorName DisplayOrder="Western"><GivenName>Jean-Raymond</GivenName><FamilyName>Abrial</FamilyName></AuthorName><Role>Consultant</Role><Contact><Email>jr@abrial.org</Email></Contact></Author><Author AffiliationIDS="Aff9"><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Cansell</FamilyName></AuthorName><Contact><Email>Dominique.Mery@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff10"><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Méry</FamilyName></AuthorName><Contact><Email>Dominique.Cansell@loria.fr</Email></Contact></Author><Affiliation ID="Aff8"><OrgAddress><City>Marseille</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>LORIA, Université Henri Poincaré Nancy 1</OrgName><OrgAddress><Postbox>BP 239</Postbox><City>Vandœuvre-lès-Nancy Cédex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>LORIA, INRIA Lorraine</OrgName><OrgAddress><Postbox>BP 239</Postbox><City>Vandœuvre-lès-Nancy Cédex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>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.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>Supported in part by PRST Intelligence Logicielle/QSL/DIXIT project and by PRST Intelligence Logicielle/QSL/ADHOC project</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Formal Derivation of Spanning Trees Algorithms</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Formal Derivation of Spanning Trees Algorithms</title></titleInfo><name type="personal"><namePart type="given">Jean-Raymond</namePart><namePart type="family">Abrial</namePart><affiliation>Marseille, France</affiliation><affiliation>E-mail: jr@abrial.org</affiliation><role><roleTerm type="text">author</roleTerm></role><description>Consultant</description></name><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Cansell</namePart><affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, Vandœuvre-lès-Nancy Cédex, France</affiliation><affiliation>E-mail: Dominique.Mery@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Méry</namePart><affiliation>LORIA, INRIA Lorraine, BP 239, Vandœuvre-lès-Nancy Cédex, France</affiliation><affiliation>E-mail: Dominique.Cansell@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2003</dateIssued><copyrightDate encoding="w3cdtf">2003</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">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.</abstract><relatedItem type="host"><titleInfo><title>ZB 2003: Formal Specification and Development in Z and B</title><subTitle>Third International Conference of B and Z Users Turku, Finland, June 4–6, 2003 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Didier</namePart><namePart type="family">Bert</namePart><affiliation>Laboratoire LSR-IMAG, CNRS, 681, rue de la Passerelle, BP 72, 38402, Saint-Martin-d’Heres Cedex, France</affiliation><affiliation>E-mail: Didier.Bert@imag.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jonathan</namePart><namePart type="given">P.</namePart><namePart type="family">Bowen</namePart><affiliation>CISM, London South Bank University, Borough Road, SE1 0AA, London, UK</affiliation><affiliation>E-mail: jonathan.bowen@sbu.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Steve</namePart><namePart type="family">King</namePart><affiliation>Department of Computer Science, University of York, YO10 5DD, Heslington, York, UK</affiliation><affiliation>E-mail: king@cs.york.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Marina</namePart><namePart type="family">Waldén</namePart><affiliation>Department of Computer Science, Åbo Akademi University, Lemminkäineng. 14 A, 20520, Turku, Finland</affiliation><affiliation>E-mail: marina.walden@abo.fi</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2003</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/3-540-44880-2</identifier><identifier type="ISBN">978-3-540-40253-4</identifier><identifier type="eISBN">978-3-540-44880-8</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">77733</identifier><identifier type="BookID">3-540-44880-2</identifier><identifier type="BookChapterCount">31</identifier><identifier type="BookVolumeNumber">2651</identifier><identifier type="BookSequenceNumber">2651</identifier><part><date>2003</date><detail type="volume"><number>2651</number><caption>vol.</caption></detail><extent unit="pages"><start>457</start><end>476</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2003</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2003</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2003</recordOrigin></recordInfo></relatedItem><identifier type="istex">A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCB</identifier><identifier type="ark">ark:/67375/HCB-6MRKL2RH-K</identifier><identifier type="DOI">10.1007/3-540-44880-2_27</identifier><identifier type="ChapterID">27</identifier><identifier type="ChapterID">Chap27</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2003</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2003</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-6MRKL2RH-K/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002633 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002633 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:A26591E4D1FB0E4E3989FC03822FF13BC3DD5BCB
|texte= Formal Derivation of Spanning Trees Algorithms
}}
| This area was generated with Dilib version V0.6.33. |  |