Integrity Constraints for Microcontroller Programming in Datalog

We consider microcontroller-programming with a declarative language based on the logic-programming language Datalog. Our prototype implementation translates a Datalog dialect to C-code for the Arduino IDE. In order to prove the correctness, one must ensure that the very limited memory of the microcontroller is sufficient for the derived facts. In this paper, we propose a class of constraints called “generalized exclusion constraints” that can be used for this task. Moreover, they are needed to exclude conflicting commands to the hardware, e.g. different output values on a pin in the same state. This class of constraints also generalizes keys and functional dependencies, therefore our results also help to prove such constraints for derived predicates.