Software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the extreme, in human lives. Software analysis is an area in software engineering concerned on the application of different techniques in order to prove the (relative) absence of errors in software artifacts. In many cases these methods of analysis are applied by following certain methodological directives that ensure better results. In a previous work we presented the notion of satisfiability calculus as a model theoretical counterpart of Meseguer's proof calculus, providing a formal foundation for a variety of tools that are based on model construction. The present work shows how effective satisfiability sub-calculi, a special type of satisfiability calculi, can be combined with proof calculi, in order to provide foundations to certain methodological approaches to software analysis by relating the construction of finite counterexamples and the absence of proofs, in an abstract categorical setting.
翻译:软件分析是软件工程的一个领域,涉及应用不同技术,以证明软件工艺品中不存在错误(相对),在许多情况下,这些分析方法是通过某些方法指令应用的,以确保更好的结果。在以前的一项工作中,我们提出了可视性计算法的概念,作为Meseguer证据计算法的理论模型,为基于模型构建的各种工具提供了正式基础。目前的工作表明,如何将可视性亚计算法(一种特殊类型的可识别性计算法)与证据计算法相结合,以便为某些软件分析方法提供依据,在抽象的直截面设置中,通过构建一定的反比标本和缺乏证据,为软件分析提供基础。