Coq

Wikipediasta
Siirry navigaatioon Siirry hakuun

Coq on funktionaalisen ohjelmointiin perustuva todistusapuri. Sen avulla voidaan laatia formaaleja matemaattisia todistuksia, jotka tarkistetaan automaattisesti. Todistukset esitetään induktiivisten konstruktioiden kalkyyliin perustuvalla Gallina-ohjelmointikielellä[1].

Coqia käytetään mm. ohjelmistojen verifiointiin ja matematiikan formalisointiin. Coq on toteutettu OCaml-kielellä.

Koodiesimerkkejä[muokkaa | muokkaa wikitekstiä]

Määritellään luonnollisten lukujen tyyppi:

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

Määritellään luonnollisten lukujen yhteenlasku:

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Osoitetaan, että määritellylle yhteenlaskufunktiolle pätee kaikilla .

Theorem plus_n_O: forall n: nat, plus n O = n.
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - trivial. simpl. rewrite IHn. reflexivity.
Qed.

Merkittäviä sovellutuksia[muokkaa | muokkaa wikitekstiä]

Lähteet[muokkaa | muokkaa wikitekstiä]

  1. What is Coq ? | The Coq Proof Assistant coq.inria.fr.
  2. Gonthier, Georges: Formal Proof—The Four- Color Theorem. Notices of the American Mathematical Society, 2008.
  3. Feit thomson proved in coq - Microsoft Research Inria Joint Centre www.msr-inria.fr. Arkistoitu 19.11.2016. Viitattu 7.12.2015. en-US

Aiheesta muualla[muokkaa | muokkaa wikitekstiä]

Tämä tietotekniikkaan liittyvä artikkeli on tynkä. Voit auttaa Wikipediaa laajentamalla artikkelia.