Problem with understanding the Mathematical Equations related to Testing Tool

Question

I have downloaded the slides from the site: [Compliance and Violation Patterns It says No writes after calls. I can understand this concept. It’s a remedy for reentrancy problem. But it shows compliance and security patterns in some technical language related to Datalog or to some language related to software representation. Can some body please guide me what is the meaning of those equations?

Zulfi.

Answer 1

They are statements about patterns of correct and incorrect code:

1. For all call sites L1, there does not exist a store site L2 such that ... (and here I’m not clear—is that L2 may follow L1? Or that the truth of the statement may follow from the program, depending on L1 and L2?)
2. For all call sites L1, there exists a store site L2 such that ... (idem.)