如何寻出Timsort算法和玉兔月球车中的Bug？
发布时间：2022-05-11 09:45:20 所属栏目：安全 来源：互联网
导读：000 背景 形式化方法(Formal Methods)在我们一般人眼中是非常高大上的东西，最多也就是当年在课堂上听说过而已，在实际工作中很少有人使用。 如何找出Timsort算法和玉兔月球车中的Bug？ 前一阵子Reddit上的一个帖子让高冷的形式化方法也上了一次头条，故事就
|
0×00 背景 形式化方法(Formal Methods)在我们一般人眼中是非常高大上的东西，最多也就是当年在课堂上听说过而已，在实际工作中很少有人使用。 如何找出Timsort算法和玉兔月球车中的Bug？ 前一阵子Reddit上的一个帖子让高冷的形式化方法也上了一次头条，故事就是国外某技术团队利用形式化方法验证了Java中一些排序算法的正确性，但是在验证Timsort排序算法时发现了Bug，于是便向Java开源社区报告了这个Bug，同时给出了经过形式化方法验证过的修复方案。本来是个皆大欢喜的结局，结果Java开源社区并没采纳他们的修复方案，而是采用了另一个Dirty Solution……(任性，就不听你的，不服你来咬我啊) 0×01 什么是Timsort 说起排序，我们比较熟悉的有冒泡、选择、插入排序，当然还有神奇的快排(Quick Sort)，Timsort是个什么鬼? Timsort算法是Tim Peters于2002年提出的一个排序算法(以自己名字命名的……)，相比其他排序算法算是后起之秀了。我们评价一个排序算法的好坏要从许多方面衡量，看看下面这张图 要理解这个Bug产生的原因，我们先来看看Timsort算法的原理 0×02 Timsort原理 简单来说，Timsort是一种结合了归并排序和插入排序的混合算法，它基于一个简单的事实，实际中大部分数据都是部分有序(升序或降序)的。 （编辑：东莞站长网） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |
站长推荐