Smart Contract Composition Operators Study Guide

Short Answer Questions

What are the two different concepts of smart contracts?

What is the main advantage of blockchains over centralized databases?

What is the main advantage of Finite Trace Linear Dynamic Logic (LDLF) over Finite Trace Linear Temporal Logic (LTL)?

What is the purpose of "protocol" in the DSL syntax described in this study material?

In the DSL semantics, how do you map properties to LDLF formulas?

Explain the three smart contract composition operators and how they work.

How are guard formulas used in automatic smart contract generation?

Describe the process of converting a smart contract into an executable state graph.

What is the purpose of endorsement policies in permissioned blockchain networks?

Explain the concept of the "block data" portion of a blockchain and how it improves on traditional data blocks.

Answers

The two different concepts of smart contracts are: 1) as a piece of code that runs on a blockchain platform, and 2) as a machine-readable agreement with legal force.

A blockchain is a decentralized, immutable, and secure storage, while traditional databases are centralized. This makes the blockchain harder to tamper with and enables trust to be established between untrusted parties.

LDLF allows regular paths to be used in formulas to specify modality, whereas LTL does not. This makes LDLF more expressive than LTL and able to express a wider range of timing properties.

A "protocol" defines a regular pattern of events that a smart contract will handle, using sequence (;), selection (+), loop (*), and test (?) operators. This is similar to regular expressions, which are defined as regular patterns of characters.

A property is a set of LDLF formulas that specify the timing constraints that a smart contract needs to satisfy. Each property maps directly to an LDLF formula, which are connected together by logical connectives.

The three composition operations are sequence, selection, and loop. The sequence operation executes two smart contracts in a defined order. The selection operation connects two smart contracts via a logical disjunction. The loop operation executes a specified smart contract a specified number of times.

Guard formulas are used in automatic smart contract generation to distinguish between the rule parts of different smart contracts in the composition operation. This ensures that the generated smart contract is consistent and meets the specification.

First, the smart contract is converted into an LDLF formula using [[.]]. The LDLF formula is then converted into a deterministic finite automaton (DFA) that accepts traces where the formula is true. Finally, the DFA is converted into an executable state graph, such as SCXML.

The endorsement policy defines which nodes are required to endorse a transaction before it is submitted to the blockchain. This ensures that only authorized parties can update the ledger and helps prevent fraud.

The block data portion stores transaction information for each block in the blockchain. Compared to traditional data blocks, it can also store events, transitions, and state information derived from SCXML. This enables new data required for the formation of smart contracts to be appended to the blockchain's immutable ledger.

Glossary

Term Definition Blockchain A distributed database that maintains a growing list of records (called blocks) that are linked together by cryptography. Smart Contract A piece of code stored on the blockchain that is automatically executed when predefined conditions are met. Finite Trajectory Linear Dynamic Logic (LDLF) A type of temporal logic that extends LTL to allow the use of regular expressions to express more complex temporal properties. Deterministic Finite Automata (DFA)A finite state machine that produces a unique computation for each input symbol. Statechart Extensible Markup Language (SCXML)An XML-based markup language that provides a general state machine-based execution environment. Combination operations are used to combine multiple smart contracts into operations of more complex smart contracts. Guard formulas are logical formulas used to distinguish the rule parts of different smart contracts in the combination operation. Endorsement policies define the rules for which nodes need to endorse a transaction before it is submitted to the blockchain. Block dataA part of each block in the blockchain that stores transaction information and other related data.