[isabelle] Sorting algorithms in the AFP



Dear all,

I stumbled over a fundamental structural issue in the AFP (referring to
the 2021 release):

* There is entry Efficient_Merge_Sort, with obvious content.

* There is theory Automatic_Refinement.Misc, which provides both a quick
sort and a merge sort specification tailored for efficient execution.

* There are a couple of references to Automatic_Refinement.Misc
throughout the AFP:

>> 	thys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Semantics.thy:7:  "Automatic_Refinement.Misc"
>> 	thys/CAVA_Automata/Digraph_Basic.thy:4:  "Automatic_Refinement.Misc"
>> 	thys/Kruskal/UGraph.thy:5:    "Automatic_Refinement.Misc"
>> 	thys/Kruskal/Kruskal_Misc.thy:5:    "Automatic_Refinement.Misc"
>> 	thys/Separation_Logic_Imperative_HOL/Assertions.thy:7:  Automatic_Refinement.Misc
>> 	thys/Separation_Logic_Imperative_HOL/ROOT:19:    Automatic_Refinement.Misc
>> 	thys/IP_Addresses/WordInterval_Sorted.thy:3:        Automatic_Refinement.Misc (*Mergesort. TODO: dependnecy! we need a mergesort afp entry!!*)
>> 	thys/IP_Addresses/ROOT:9:    Automatic_Refinement.Misc (* mergesort *)
>> 	thys/Refine_Imperative_HOL/Lib/Pf_Add.thy:2:imports Automatic_Refinement.Misc "HOL-Library.Monad_Syntax"
>> 	thys/DFS_Framework/Misc/DFS_Framework_Misc.thy:2:imports Automatic_Refinement.Misc
>> 	thys/Flow_Networks/Lib/Fofu_Abs_Base.thy:5:  Automatic_Refinement.Misc
>> 	thys/Network_Security_Policy_Verification/Lib/Efficient_Distinct.thy:3:  Automatic_Refinement.Misc (*mergesort*)
>> 	thys/Collections/Lib/Dlist_add.thy:5:  Automatic_Refinement.Misc
>> 	thys/Collections/Lib/Sorted_List_Operations.thy:3:imports Main Automatic_Refinement.Misc
>> 	thys/Collections/Iterator/SetIterator.thy:8:  Automatic_Refinement.Misc 
>> 	thys/LOFT/LinuxRouter_OpenFlow_Translation.thy:3:  Automatic_Refinement.Misc (*TODO@Peter: rename and make available at better place :)*)
>> 	thys/Tree-Automata/Ta.thy:7:imports Main Automatic_Refinement.Misc Tree
>> 	thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy:6:        Automatic_Refinement.Misc (*dependnecy!*)

I have not yet visited all of them in detail but already this overview
suggests that a significant amount of those references makes use of the
sorting algorithms.

It seems worth a try whether those applications can be changed to use
session Efficient_Merge_Sort instead.  But maybe the authors /
maintainers of Automatic_Refinement can say more on this.

In any case, the sorting part of Automatic_Refinement.Misc should be
made more explicit using a separate theory.

Cheers,
	Florian

Attachment: OpenPGP_signature
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.