Javachecker: статический анализ программных комплексов с помощью переписывающих правил

Abstract

У роботі описано один із підходів до аналізу програмних комплексів, що грунтується на методех символьної обробки інформації. Особливістю підходу є застосування формального аналізу не до обчислювальної семантики програмних систем, а до окремих характеристик. Це дозволяє уникнути складнощів повної формалізації задачі, і у той-же час дозволяє проводити прагматично корисні висновки щодо характеристик програмної системи (такі, як наявнісьт помилок визначенного классу) за допомогою порівняльно невеликого об'єму обчислень. Описується статичний аналізатор програм на мові Java (JavaCheker), що реалізує даний підхід і побудован у середовищі алгебраїчного програмування TermWare.

This work describeі an approach to software system analysis, based on the methods of symbolic comutations. The approach is characterized by using light-weight formal model based not on full-fledged computation semantics, but on particular properties of underlying software system. Such approach eliminate need in full formal analysis of software system and allows to receive some pragmatically usefull results about software (such as existence of some types of errors) without complex comutations. Static analyzer for Java source code (JavaChecker) build on top of TermWare framework is described.