几天前，Facebook工程团队表现出色-被授予“
最具影响力的POPL论文奖” 。 在机器学习专家中，这是非常光荣的。 该奖项是针对
通过诱拐进行
成分形状分析而颁发的，该奖项揭示了Project Infer的细微差别。 该项目本身旨在在部署之前检测并消除移动应用程序代码中的错误。
移动设备软件中的错误对于开发人员和用户而言都是非常昂贵的。 对于第一个问题，对于任何专家来说，检测目录中已有应用程序中的问题是一场噩梦。 当然，要对软件进行测试，并根据某些模板检查程序的工作。 但是更常见的是，开发人员无法预见一切，并且在部署后会检测到应用程序中的错误。
我们提醒您： 对于所有“哈勃”读者来说，使用“哈勃”促销代码注册任何Skillbox课程时均可享受10,000卢布的折扣。
Skillbox建议： Python数据分析师在线课程。
Project Infer扫描移动应用程序的代码，并允许您查找各种问题，其模式存储在数据库中（并且始终在更新中）。 该项目本身是三年前提出的。 公告发布后，Facebook几乎立即打开了代码，此后便开始在Amazon Web Services，Spotify和Uber等公司中使用。
如何运作？
Project Infer使用一组专门的算法来分析代码的操作。 任何大型应用程序的源代码中可能有数百万种组合，它们可能导致错误。 传统的代码分析过程无法帮助检测所有内容。 从Facebook推断，自学习正在扩展其基础，因此该项目使您可以检测代码中的许多问题。
从一般意义上讲，Facebook推断过程可以分为两个阶段：数据收集和分析。 生命周期也分为两个部分：全局和差分。
在数据收集阶段，Infer将源代码翻译成自己的语言。 分析阶段专用于研究代码结构的最小细节，这有可能导致出现错误。 如果Infer遇到已识别为错误模式的因素的已经很熟悉的组合，则针对特定方法或功能的分析将停止，但是将继续分析其他方法和功能。 这是一个推断的例子。
从执行的角度来看，如上所述，Infer可以以两种方式工作-全局和差异。 在第一种情况下，Infer将分析所有文件。 对于使用Gradle编译的项目，使用以下命令启动Infer
infer run -- gradle build
差异过程用于特定于移动应用程序的增量构建系统中。 在这种情况下，您必须首先开始收集Infer数据以获取所有编译命令，然后仅分析更改。 为此，请使用以下命令集：
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
可以使用InferTraceBugs命令查看推断报告。
infer run -- gradle build inferTraceBugs
项目推断基金会
Facebook的推断基于两种新的数学方法：
分离逻辑和
双绑架 。
分离逻辑的关键特征是局部推理的可能性。 它的出现是由于在堆的各个部分之间存在空间连接词的陈述。 在这种情况下，无需考虑每个阶段的全部内存量。
分隔逻辑的主要元素是*运算符（或单独地），它称为拆分连接。 公式X↦Y∗Y↦X可以理解为“ X指向Y，而Y分别指向X”，这与内存指针的工作原理非常相似。
在“推理双拐”的上下文中，可以将其视为一种推理方法，该方法使平台能够检测与应用程序代码的独立部分的行为有关的属性。 双绑架一起显示反框架（状态的缺失部分）和框架（不受操作影响的那些部分）。 在数学上，双向绑架问题使用以下语法表示：A *？ ⊢B* 框架。
在Facebook的Infer上，只要我们知道基本代码级别的基元规范，该方法就可以从纯净代码中得出pre / post规范。
由于对机器学习专家的工作进行了多年的分析，因此FI的创建成为可能。 在有关Infer的工作过程中，针对整个领域发布了以下关键文章：
- 用双外展法进行成分形状分析 。 仅出于这项工作，就收到了奖品，如上所述。 该作品向读者介绍了表格的成分分析。 这是对传统形状分析的补充，传统形状分析使应用该方法分析应用程序源代码成为可能。
- 基于分离逻辑的局部形状分析 ：本文将分离逻辑描述为一种分析应用程序源代码的机制。 作者展示了在不检查整个堆整体的情况下研究内存堆中单个单元的可能性。 因此，某些单元格无需完整分析即可构成一个链表。
- Smallfoot：具有分离逻辑的模块化自动断言检查 ：本文介绍了名为Smallfoot的Facebook Infer前身。
- AL：一种用于使用Infer检测错误的新的声明性语言 ：AL允许任何开发人员在不完全了解Infer内部厨房的情况下设计新的检查器。 AL是一种声明性语言。
- 通过软件验证快速发展 ：最后，一篇文章揭示了Facebook如何根据自己的需求使用Project Infer。 该文档讨论了Facebook开发人员如何将Infer集成到他们的开发过程中，从而为移动应用程序（如Instagram，Facebook Messenger和适用于Android和iOS的Facebook应用程序）提供静态分析。
到目前为止，Infer只能用于移动应用程序。 但是它的某些原理适用于通用应用程序。 也许将来Infer的可能性会越来越广泛，借助它的帮助，开发人员将能够分析台式机或服务器应用程序。
Skillbox建议：