FinProof
Bug-free financial services platform
Integration of proven modules into the existing systems
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
Fixpoint insert (n:Z) (ms : zlist) {struct ms} : zlist :=
match ms with
| 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 (sort ms')
end.
Definition head {X} (a: X) (l: list X) : X :=
match l with
| [] => a
| x:: _ => x
end.
Inductive sorted : zlist -> Prop :=
| sortnil: sorted []
| sortcons: forall a m, sorted m -> a <= (head a m) -> sorted (a :: m).
match ms with
| 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 (sort ms')
end.
Definition head {X} (a: X) (l: list X) : X :=
match l with
| [] => a
| x:: _ => x
end.
Inductive sorted : zlist -> Prop :=
| sortnil: sorted []
| sortcons: forall a m, sorted m -> a <= (head a m) -> sorted (a :: m).
Lemma insertdiv: 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.
Theorem sort_perm: forall (l: zlist),
Permutation l (sort l).
Proof.
intros. induction l.
simpl. constructor.
simpl. assert (exists l' l'', insert a (sort l) = l' ++ [a] ++ l'' /\ sort l = l' ++ l'').
apply insertdiv. inversion H. inversion H0. inversion H1.
rewrite H2. apply perm_trans with (l':= a::(x++x0)).
constructor. rewrite <- H3. auto. apply Permutation_cons_app.
apply Permutation_refl.
Qed.
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.
Theorem sort_perm: forall (l: zlist),
Permutation l (sort l).
Proof.
intros. induction l.
simpl. constructor.
simpl. assert (exists l' l'', insert a (sort l) = l' ++ [a] ++ l'' /\ sort l = l' ++ l'').
apply insertdiv. inversion H. inversion H0. inversion H1.
rewrite H2. apply perm_trans with (l':= a::(x++x0)).
constructor. rewrite <- H3. auto. apply Permutation_cons_app.
apply Permutation_refl.
Qed.
Our mentors
Contact us
