Joulukalenteri 2009: SPARK

Kirjoittaja: Schedler (18.12.2009)

SPARK on erityisen suurta luotettavuutta ja turvallisuutta (sekä safety että security) vaativien järjestelmien kehittämiseen tarkoitettu ohjelmointikieli. Kielen kehitystyö alkoi Englannissa 80-luvulla, jolloin todettiin ettei tarkoitukseen soveltuvaa kieltä ollut vielä olemassa. Kielen perustaksi valittiin Ada, josta oli jo tuolloin saatavilla kansainvälinen standardi. Lisäksi Adan vahva tyyppijärjestelmä ja modulaarisuutta tukevat piirteet nähtiin hyödyllisiksi.

Koska SPARK perustuu Adaan, kaikki SPARK-ohjelmat ovat myös laillisia Ada-ohjelmia. Näinollen SPARK-ohjelmien kääntäminen onnistuu kaikilla Ada-kääntäjillä.

Johtuen kielen suunnitellusta käyttötarkoituksesta, saattaa kieli vaikuttaa primitiiviseltä moneen nykyiseen kieleen verrattuna. Kielestä on tarkoituksella jätetty pois mm. tuki rekursiivisille funktioille, sekä dynaaminen muistinhallinta. Tyypillisiä SPARKin sovellusalueita ovat mm. lentokoneiden sekä helikopterien ohjausjärjetelmät, sekä kryptografiset sovellukset.

Esimerkki: Tekstin tulostus

Tulostetaan "Hello, World!":

with Spark_IO;
--# inherit Spark_IO;

--# main_program;
procedure Main
  --# global in out SPARK_IO.Outputs;
  --# derives SPARK_IO.Outputs from *;
is
begin -- Main
   Spark_IO.Put_String(File  => Spark_IO.Standard_Output,
                       Item  => "Hello, World!",
                       Stop  => 0);
   Spark_IO.New_Line(File    => Spark_IO.Standard_Output,
                     Spacing => 1);
end Main;

SPARK vaatii tarkempiin ohjelman staattisiin analyyseihin annotaatioita, jotka on merkitty --# -merkkiyhdistelmällä. Esimerkissä "inherit Spark_IO" ilmaisee sen, että pääohjelmassa käytetöön Spark_IO-pakettia.

Esimerkki: Fibonaccin luvut

with Spark_IO;
--# inherit Spark_IO;

--# main_program;
procedure Fib_Ex
  --# global in out SPARK_IO.Outputs;
  --# derives SPARK_IO.Outputs from *;
is
   Result : Natural;
   I      : Natural := 1;

   function Fibonacci(N : Natural) return Natural
     --# pre (N >= 0);
   is
      Fib   : Natural := 1;
      Fib_1 : Natural := 1;
      Fib_2 : Natural := 0;
      K     : Natural := 0;
   begin
      while K < N
	--# assert (K >= 0) and (K < N);
      loop
         Fib   := Fib_1 + Fib_2;
         Fib_2 := Fib_1;
         Fib_1 := Fib;
         K := K + 1;
      end loop;

      return Fib;
   end Fibonacci;

begin -- Fib_Ex
   Result := Fibonacci(I);
   while Result <= 100 loop
      Spark_IO.Put_Integer(File  => Spark_IO.Standard_Output,
                           Item  => Result,
                           Width => 3,
                           Base  => 10);
      Spark_IO.New_Line(File     => Spark_IO.Standard_Output,
                        Spacing  => 1);

      Result := Fibonacci(I);
      I      := I + 1;
   end loop;
end Fib_Ex;

Esimerkki: Laitteistoläheinen ohjelmointi

Koska SPARK perustuu Ada-kieleen, on siinä erinomainen tuki laitteistoläheiseen ohjelmointiin. Alla esimerkki SPARKilla toteutetusta A/D-muuntimen ajurista:

package AD
  --# own in Input;
is
   type Val_T is range 0..2**8-1;  -- 8-bittinen tulos AD-muuntimen arvolle
   procedure Read(Val : out Val_T);
   --# global in Input;
   --# derives Val from Input;
end AD;

package body AD is
   Input: Val_T;
   for Input'Address use 16#0800_0001#;

   procedure Read(Val : out Val_T) is
   begin
      Val := Input;
   end Read;
end AD;

AD-muunnin on esimerkissä esitetty yhtenä pakettina (package), joka sisältää Read-aliohjelman hetkellisen muuntimen arvon lukemiseen. Tietovuoanalyysin tukemiseksi annotaation "own in Input" kertoo että AD-muuntimen tila saa arvonsa laitteistosta käsin. AD-muuntimen hetkellinen arvo luetaan muistiosoitteesta 0800_0001(hex).

Linkkejä

SPARK-kotisivu
Wikipedia-artikkeli SPARKista