Re: [isabelle] Sorting algorithms in the AFP



Hi Florian,

I don't understand what the fundamental issue is there.

Do you mean that all entries should use only one specific sort implementation? (Why?) Or is it that the one in Automatic_Refinement is hard to reference?

Cheers,
Gerwin

> On 16 Jun 2021, at 21:19, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> 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: signature.asc
Description: Message signed with OpenPGP



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