کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
432223 | 688828 | 2016 | 18 صفحه PDF | دانلود رایگان |
• We discuss specific classes of relations which allow to model the essential constituents of graphs.
• We introduce an axiomatic characterisation of the cardinality of relations.
• We derive fundamental properties on cardinalities.
• We formally verify four relational approximation algorithms by combining relation algebra and program assertions.
First, we discuss three specific classes of relations, which allow to model the essential constituents of graphs, such as vertices and (directed or undirected) edges. Based on Kawahara's characterisation of the cardinality of relations we then derive fundamental properties on their cardinalities. As main applications of these results, we formally verify four relational programs, which implement approximation algorithms by using the assertion-based method and relation-algebraic calculations.
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 2, February 2016, Pages 269–286