Bug-free financial services platform Integration of proven modules into the existing systems
How we develop bug-free software
1
The strict specification
While using FinProof the customer presents mathematically strict specification to the developer
2
Bug-free code development
Using the strict specification the developer implements it using Coq, Idris or Agda languages. The implemented code is being proved by the system that eliminates the possibility of bugs
3
No need to test the code
Due to mathematical proving of the code properties there is no need to test it that dramatically speeds up the process of software development
Strict specification & proof samples
Fixpointinsert (n:Z) (ms : zlist) {structms} : zlist := match mswith | nil => [n] | m :: ms' => if (n<=?m) then (n::ms) else (m:: (insert n ms')) end.
Fixpoint sort (ms : zlist) : zlist := match ms with | [] => [] | m::ms' => insert m (sortms') end.
Definition head {X} (a: X) (l: listX) : X := match
l with | [] => a | x:: _ => x end.
Inductive sorted : zlist -> Prop := | sortnil: sorted[] | sortcons: foralla m, sorted m -> a<= (heada m) -> sorted (a:: m).
Lemmainsertdiv: forall x l, exists l' l'', insert x l = l' ++[x]++ l'' /\ l = l' ++ l''. Proof. intros. induction l. simpl. exists [], []. split; auto. simpl. remember (x<=?a). destruct b. exists [], (a::l). split; auto. inversion IHl. inversion H. inversion H0. rewrite H1. exists (a::x0), x1. split; auto. simpl. rewrite H2. auto. Qed.