Verifying properties of a financial contract in Elixir
source link: https://elixirforum.com/t/verifying-properties-of-a-financial-contract-in-elixir/48327
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Verifying properties of a financial contract in Elixir
Welcome to the Elixir Forum!
There’s no time like the present to jump into Elixir - the functional language that’s taking the programming world by storm
As well as catering to the community’s more general needs, we have a strong focus on learning, so if you’ve been curious about Elixir or are just starting out - join up - you’ll be in great company!
This forum is also driven by the community. The more you participate here, the more trust you’ll earn and the more mod-type tools you’ll unlock - our way to reward regular members and your way to help give back to the community.
That’s not all, we have lots of other features and some really cool monthly giveaways… so what are you waiting for? Take a sip of Elixir, sign up and join in the fun
Hi, I am interested in verifying properties of Elixir code. In particular, I write code for financial institutions and I am exploring if formal verification can be useful for me.
A loan contract starts in a unsigned state, waiting for some party to propose an amount.
When an amount is proposed, the contract enters a state when it waits for signatures from lender and lendee.
Whenever an amount is proposed, both signatures are reset, so that a lendee never has to pay more than he agreed to, because every time the amount is changed, new signatures are needed.
The contract is done when all debt has been paid (and not more).
Is there an easy-to-use solution for verifying this property in the Elixir/Erlang ecossystem?
The answer might rely on property-based testing, as long as it is exhaustive up to a given measure, as in bounded model checking.
My code is:
defmodule Loan do
def start() do
spawn(__MODULE__, :main_loop, [:unsigned])
end
def main_loop(:done) do
receive do
:show ->
IO.puts("Contract is finished")
apply(__MODULE__, :main_loop, [:done])
end
end
def main_loop(:unsigned) do
receive do
{:propose, amount} ->
apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: false, lender: false]])
end
end
@spec main_loop(:proposal, any, [{:lendee, any} | {:lender, any}, ...]) :: any
def main_loop(:proposal, amount, lendee: true, lender: true) do
IO.puts("Contract is now signed, contract value is #{amount}")
apply(__MODULE__, :main_loop, [:signed, amount])
end
def main_loop(:proposal, amount, lendee: lendee, lender: lender) do
receive do
:sign_lendee ->
apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: true, lender: lender]])
:sign_lender ->
apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: true]])
{:propose, amount} ->
apply(__MODULE__, :main_loop, [:proposal, amount, lendee: false, lender: false])
:show ->
case {lendee, lender} do
{false, false} ->
IO.puts("No one has signed, contract value is #{amount}")
{false, true} ->
IO.puts("Lender has signed, contract value is #{amount}")
{true, false} ->
IO.puts("Lendee has signed, contract value is #{amount}")
{true, true} ->
IO.puts("Both lender and lendee have signed, contract value is #{amount}")
end
apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: lender]])
end
end
def main_loop(:signed, balance) when balance > 0 do
receive do
:show ->
IO.puts(balance)
apply(__MODULE__, :main_loop, [:signed, balance])
{:pay, amount} when amount <= balance ->
IO.puts("Paying #{amount} to lender")
apply(__MODULE__, :main_loop, [:signed, balance - amount])
end
end
def main_loop(:signed, 0) do
IO.puts("Contract is finished")
main_loop(:done)
end
end
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK