Facebook新推出AL語言，意在簡化程式靜态分析

al是一種易用的聲明式程式設計語言，适用于抽象文法樹（ast）推理，使開發人員可以擴充facebook infer靜态分析器的功能。

infer采用ocaml編寫，可辨別null指針通路、資源和記憶體洩漏，以及其它一些c、java和objective-c代碼中的可檢測錯誤。據facebook介紹，在他們的ios和android移動應用中，80%的軟體缺陷是由infer正确地檢測出的。

al易于擴充，這克服了一個局限infer的問題。實作擴充不僅需要具備靜态分析的專門技能驗，而且需要掌握infer的内部機制。具體而言，al意在簡化對過程内（intra-procedural）軟體缺陷新類型分析程式（checker）的定義，即局限于過程代碼内的軟體缺陷。這類軟體缺陷可使用更簡單的分析手段檢測到，包括借助于程式文法、通用語言習語和自定義約定。舉個例子，在objective-c中，為避免存留環路，對象的delegate通常不應做為strong引用。針對需求的分析程式可使用al定義為：

define-checker strong_delegate_warning = { let name_contains_delegate = declaration_has_name(regexp("[dd]elegate")); set report_when = when name_contains_delegate and is_strong_property() holds-in-node objcpropertydecl; set message = "property or ivar %decl_name% declared strong"; set suggestion = "in general delegates should be declared weak or assign"; };

在上面的al代碼中，亮點在report_when語句。該語句在objcpropertydecl對象上定義了一個條件，聲明為一個strong引用（is_strong_property）。objcpropertydecl對象就是關聯到objective-c屬性定義的ast節點。

據facebook介紹，通常使用數行al代碼就能新定義一個分析程式，并可立即投入使用，無需重新建構infer，確定了對新分析程式的快速回報。al還支援定義基于時态邏輯模型的更複雜公式，其中一個ast節點可關聯到時間上某一點，其所有的後代節點均看作是未來可驗證的。例如，為保證程式的正确性，holds-eventually所關聯的表達式可在未來某個時間點上得以驗證。

al是infer的一個組成部分，已開源于github上，适用于c、c++和objective-c。

本文轉自d1net（轉載）