声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：11-2560/TP
国际刊号：1000-9825
发布日期:
作者：左正康，黄志鹏，黄箐，孙欢，曾志城，胡颖，王昌晶
单位：左正康，江西师范大学 计算机信息工程学院, 江西 南昌 33002211,黄志鹏，江西师范大学 计算机信息工程学院, 江西 南昌 33002202,黄箐，江西师范大学 计算机信息工程学院, 江西 南昌 33002203,孙欢，江西师范大学 数字产业学院, 江西 上饶 33400604,曾志城，江西师范大学 计算机信息工程学院, 江西 南昌 33002205,胡颖，江西师范大学 计算机信息工程学院, 江西 南昌 33002206,王昌晶，江西师范大学 计算机信息工程学院, 江西 南昌 33002207
关键词：LLRB;函数式建模;机械化验证;Isabelle定理证明器;二叉搜索树
基金：国家自然科学基金(61862033, 62262031); 江西省自然科学基金(20212BAB202018); 江西省教育厅科技重点项目(GJJ210307)
基于机器定理证明的形式化验证技术不受状态空间限制, 是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法. LLRB (left-leaning red-black trees)是一种二叉搜索树变体, 其结构比传统的红黑树添加了额外的左倾约束条件, 在验证时无法使用常规的证明策略, 需要更多的人工干预和努力, 其正确性验证是一个公认的难题. 为此, 基于二叉搜索树类算法Isabelle验证框架, 对其附加性质部分进行细化, 并给出具体化的验证方案. 在Isabelle中对LLRB插入和删除操作进行函数式建模, 对其不变量进行模块化处理, 并验证函数的正确性. 这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证, 相较于目前LLRB算法的Dafny验证, 定理数由158减少至84, 且无需构造中间断言, 减轻了验证的负担; 同时, 为复杂树结构算法的函数式建模及验证提供了一定的参考价值.
来源：2024年第11期
《软件学报》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。