[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 22 May 2015 06:24:21 -0700 (PDT)

Let's take an example.

Suppose an algorithm that takes a graph an returns the nodes of the graph.

So GraphType = SUBSET [ in -> STRING, out -> STRING ]

Nodes(A) == { x \in STRING : \E n \in A : x = n.in \/ x = n.out}

Suppose G is a constant.

And resu a variable.

So the contract of the algorithm is:

Requires == G \in GraphType

Ensures == resu =Nodes(g)

So how can we link formally the contract and the algorithm? This way?

Correctness == Requires /\ Spec => [] ( pc = "Done" => Ensures )

--

FL

- Prev by Date:
**Re: Symmetry and Liveness** - Next by Date:
**Re: Symmetry and Liveness** - Previous by thread:
**Re: [tlaplus] TLC footprint value already on disk** - Next by thread:
**BagOfAll? SetOfAll?** - Index(es):