loading...
Generating Algorithms plus Loop Invariants by Formal Derivation
May 14-May 16
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICIS.2008.34Seventh IEEE/ACIS International Confe ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Haihe Shi, Dawei Du, Jinyun Xue, "Generating Algorithms plus Loop Invariants by Formal Derivation," Computer and Information Science, ACIS International Conference on, pp. 496-501, Seventh IEEE/ACIS International Conference on Computer and Information Science (icis 2008), 2008.
 
 
BibTex
x
 
@article{ 10.1109/ICIS.2008.34,
author = {Haihe Shi and Dawei Du and Jinyun Xue},
title = {Generating Algorithms plus Loop Invariants by Formal Derivation},
journal ={Computer and Information Science, ACIS International Conference on},
volume = {0},
year = {2008},
isbn = {978-0-7695-3131-1},
pages = {496-501},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICIS.2008.34},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer and Information Science, ACIS International Conference on
TI - Generating Algorithms plus Loop Invariants by Formal Derivation
SN - 978-0-7695-3131-1
SP496
EP501
A1 - Haihe Shi,
A1 - Dawei Du,
A1 - Jinyun Xue,
PY - 2008
KW - null
VL - 0
JA - Computer and Information Science, ACIS International Conference on
ER -
 
We advocate a mechanical derivation approach for developing provably correct algorithmic programs. The paper presents our new formal methods and techniques for generating algorithms plus loop invariants. Through our methods and techniques, the ideas behind MergeSort algorithm is revealed naturally from a formal specification, and then its loop invariant and nonrecursive algorithmic solution are generated mechanically. Furthermore, instead of fresh formal derivation, the Insertion Sort is easily achieved based on the derivation of MergeSort. By means of our tools their executable language programs can be generated automatically. Therefore mathematical knowledge required by formal development process is reduced substantially and the confidence in the resultant code is increased.
Citation:
Haihe Shi, Dawei Du, Jinyun Xue, "Generating Algorithms plus Loop Invariants by Formal Derivation," icis, pp.496-501, Seventh IEEE/ACIS International Conference on Computer and Information Science (icis 2008), 2008
Usage of this product signifies your acceptance of the Terms of Use.