FinProof
Внедрение доказанных модулей в действующие системы
Платформа для создания безошибочных финансовых сервисов


FinProof
Платформа для создания безошибочных финансовых сервисов
Внедрение доказанных модулей в действующие системы
Как разработать безошибочное программное обеспечение?
1
Формулирование строгой спецификации
При использовании системы FinProof заказчик предоставляет разработчику математически строго составленную спецификацию.
2
Написание безошибочного доказанного кода
По сформулированной спецификации разработчик создает программное обеспечение на языках Coq, Idris, Agda. При этом написанный код доказывается в процессе написания системой, что не позволяет разработчику допустить ошибку при разработке ПО
3
Готовая система не нуждается в тестировании
Благодаря применяемым в FinProof математическим доказательствам свойств кода в процессе разработке продукта исчезает необходимость его тестирования, что значительно ускоряет появление рабочего программного обеспечения
1
Формулирование строгой спецификации
При использовании системы FinProof заказчик предоставляет разработчику математически строго составленную спецификацию.
Как разработать безошибочное программное обеспечение?
Написание безошибочного доказанного кода
По сформулированной спецификации разработчик создает программное обеспечение на языках Coq, Idris, Agda. При этом написанный код доказывается в процессе написания системой, что не позволяет разработчику допустить ошибку при разработке ПО
2
Готовая система не нуждается в тестировании
3
Благодаря применяемым в FinProof математическим доказательствам свойств кода в процессе разработке продукта исчезает необходимость его тестирования, что значительно ускоряет появление рабочего программного обеспечения
Написание безошибочного доказанного кода
Готовая система не нуждается в тестировании
Строгая спецификация
Строгая спецификация
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).
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.
Наши менторы
Наши контакты
8 (800) 100-14-66
team@finproof.io

Наша группа в Facebook
Made on
Tilda