改进(计算)

改进是计算机科学的通用术语,它涵盖了制作正确的计算机程序并简化现有程序以实现正式验证的各种方法。

程序的完善

形式方法中,程序的完善是将摘要(高级)形式规范变成具体(低级)可执行程序可验证转换。逐步完善允许在阶段完成此过程。从逻辑上讲,改进通常涉及含义,但可能还有其他并发症。

敏捷软件开发方法(例如Scrum )中产品积压(需求列表)的渐进性即时准备也通常被描述为改进。

数据完善

数据改进用于将抽像数据模型(例如集合)转换为可实现的数据结构(例如数组)。操作改进将系统上操作的规范转换为可实施程序(例如,过程)。在此过程中,后条件可以加强和/或前提条件削弱。这通常减少了规范中的任何非确定主义,通常是完全确定性的实现。

例如,可以将x∈ {1,2,3}(其中x是操作后变量x的值)可以改进到x∈ {1,2},然后是x∈ {1},并以x :: = 1 . x := 2和x := 3的实现在这种情况下,使用不同的途径进行改进。但是,我们必须小心不要精炼x∈ {}(等效于false ),因为这是无法实现的。从空集中选择一个成员是不可能的。

有时还会使用重新化术语(由Cliff Jones创造)。如果不可能进行正式完善,则裁员是一种替代技术。改进的相反是抽象

改进演算

改进演算是一种正式的系统(灵感来自Hoare Logic ),可促进计划的改进。 Fermat转换系统是改进的工业强度实施。 B-Method也是一种正式的方法,可扩展使用组件语言的细化演算:它已用于工业发展。

改进类型

类型理论中,改进类型是一种具有谓词的类型,该类型假定适用于精制类型的任何元素。当用作函数参数后条件,改进类型可以表达前提条件:例如,接受自然数并返回自然数大于5的函数的类型可以写为5 。因此,改进类型与行为亚型有关。

也可以看看