The Hoare-fol Tool

TL;DR

Hoare-fol is a software tool that applies Hoare logic and Dijkstra's calculus to analyze biological regulatory networks, enabling computation, simplification, and solution generation for complex logical models.

Contribution

It implements a theoretical framework for analyzing biological networks using Hoare logic, including features for weakest precondition computation, simplification, and ASP translation.

Findings

Successfully computes weakest preconditions for biological models

Simplifies logical conditions using De Morgan laws and partial knowledge

Translates problems into Answer Set Programming for solution finding

Abstract

This document presents the tool named ''Application of Hoare Logic and Dijkstra's Weakest Proposition Calculus to Biological Regulatory Networks Using Path Programs with Branching First-Order Logic Operators'' or Hoare-fol for short. This tool consists in an implementation of the theoretical work developed in [Bernot et al., 2019] and contains the following features: (1) computation of the weakest precondition of a Hoare triple, (2) simplification of this weakest precondition using De Morgan laws and partial knowledge on the initial state, and (3) translation into Answer Set Programming to allow a solving of all compatible solutions.