I am currently reading the extended Version of the Paper Online Detection of Effectively Callback Free Objects with Applications of Smart Contract.

I am trying to understand the proofs of Chapter 6. In particular, I cannot understand the premise of proofs 6.2. Indeed, the authors use a variant of SMAC, an Object-oriented and Turing Complete (SMAC) and they claim that (I underlined the suspicious claim with bold)

Thus, we focus on verifying $sECF$, namely, statically verifying whether all executions of an object are $dECF_{FS}$ or $ECF_{C}$, where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA). Such a PDA for an object o is able to simulate any modular well-formed execution $\kappa \in \pi$ where the active object of all states in $\pi$ is o.

In my understanding, this premise should be wrong, because although the state of this SMAC program is final, it is not computable by Push-Down-Automata (which compute total functions).

Foo:
     int x = 0 // field of the object
     enter // enter the single method of the object/contract
         while true do 
             x = 1
     return

This question had a bounty worth +100 reputation from Briomkez that ended 3 hours ago. Grace period ends in 20 hours

This question has not received enough attention.

where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA).

You are correct that if you understand it as using a pushdown-automaton to model the full behavior of the object, since as you indicated, you can put a Turing complete Turing machine inside any object.

However, I would believe that the authors intend to use a pushdown-automaton to mode an object in the domain with its possible states as defined by the values of its fields and its execution stack, since the whole paper is focusing on the ECF(Effectively Callback Free) property for objects. The actual moments when the object is still in the middle of changing from one state to another state are ignored/irrelevant/transparent/skipped. More specifically, the following shows the purpose of the object.

Such a PDA for an object o is able to simulate any modular well-formed execution $\kappa \in \pi$ where the active object of all states in $\pi$ is o

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.