Раздельная верификация объектно-ориентированных программ с построением протокола С++ класса в терминах сетей Петри

Формальное доказательство корректности программ является единственным надежным методом обеспечения правильного функционирования программных систем. Существующие методы верификации программ на практике довольно сложны, и это препятствует их повсеместному применению. В настоящей статье предлагается подход, применяющий концепцию “Design By Contract”, в котором протоколы классов, сформулированные в терминах сетей Петри, позволяют проводить анализ классов и программ раздельно, что облегчает проверку работоспособности объектно-ориентированных программ.