I have downloaded the slides from the site: Compliance and Security 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 somebody please guide me what is the meaning of those equations?
Some of these symbols come from Predicate Logic. The
∀ means "For all" and the
∃ means "There exists." The
¬ indicates negation.
I'm guessing the Compliance pattern is something like:
For all calls of the form (L_1,_ ,_), there exists no such store (L_2,_ ,_)...
If you can link where you downloaded your slides from, we may have more clues into what the other terms mean.