Retranscription of zilliqa’s auction contract:
https://github.com/Zilliqa/scilla/blob/master/tests/contracts/auction.scilla
auction_zilliqa.arlarchetype auction_zilliqavariable highest_bid : tez = 0tzvariable highest_bidder : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jgvariable beneficiary : address = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWkasset pending_return identified by incumbent {incumbent : address;val : tez;}states =| Open initial| Closedvariable auction_start : date = 2019-01-01T00:00:00variable auction_end : date = 2019-02-01T00:00:00specification {contract invariant highest_is_not_pending {not (pending_return.contains(highest_bidder))}contract invariant highest_is_highest {forall pr in pending_return,pr.val <= highest_bid and pr.incumbent <> highest_bidder}}entry place_bid () {require {c1 : auction_start <= now <= auction_end;}effect {if pending_return.contains(caller)then (var bid = pending_return[caller].val;var new_bid = bid + transferred;if new_bid > highest_bidthen ((* update pending_return *)pending_return.add ({ incumbent = highest_bidder;val = highest_bid });pending_return.remove(caller);(* update highest *)highest_bid := new_bid;highest_bidder := caller)elsepending_return.update (caller, { val = new_bid }))elseif caller = highest_bidderthen(* caller is highest_bidder! accumulate *)highest_bid += transferredelse if transferred > highest_bidthen ((* update pending_return *)pending_return.add ({incumbent = highest_bidder;val = highest_bid });(* update highest *)highest_bid := transferred;highest_bidder := caller)else fail ("no update") (* no need to add bidder since there willbe nothing to withdraw *)}}(* onlyonce extension specifies that one cannot withdraw more than once *)entry withdraw () {specification {variable call_count : int = 0shadow effect {call_count += 1}postcondition o1 {pending_return.contains(caller) -> call_count = 0}postcondition o2 {call_count <= 1}}require {c2 : pending_return.contains(caller);}effect {transfer pending_return[caller].val to caller;pending_return.remove(caller)}}transition endAuction () {from Opento Closedwhen { now > auction_end }with effect {transfer highest_bid to beneficiary}}