SPARK (programlama dili) - SPARK (programming language)

Bu makale programlama dili ile ilgili . İçin küme bilgisayar üzerinde çalışabilir çerçeve Scala , Java ve Python , bkz Apache Spark .
KIVILCIM
kıvılcım.jpg
paradigma çok paradigma
geliştirici Altran ve AdaCore
kararlı sürüm
Topluluk 2021 / 1 Haziran 2021 ; 4 ay önce ( 2021-06-01 )
Yazma disiplini statik , güçlü , güvenli , yalın
işletim sistemi Çapraz platform : Linux , Microsoft Windows , Mac OS X
Lisans GPLv3
İnternet sitesi SPARK hakkında
Başlıca uygulamalar
SPARK Pro, SPARK GPL Sürümü, SPARK Topluluğu
Tarafından etkilenmiş
Ada , Eyfel

SPARK , öngörülebilir ve son derece güvenilir operasyonun gerekli olduğu sistemlerde kullanılan yüksek bütünlüklü yazılımların geliştirilmesi için tasarlanmış , Ada programlama diline dayalı, resmi olarak tanımlanmış bir bilgisayar programlama dilidir . Emniyet, güvenlik veya iş bütünlüğü talep eden uygulamaların geliştirilmesini kolaylaştırır.

Başlangıçta, sırasıyla Ada 83, Ada 95 ve Ada 2005'e dayanan SPARK dilinin (SPARK83, SPARK95, SPARK2005) üç versiyonu vardı.

SPARK dilinin dördüncü versiyonu olan SPARK 2014, Ada 2012'ye dayalı olarak 30 Nisan 2014'te yayınlandı. SPARK 2014, dilin ve destekleyici doğrulama araçlarının tamamen yeniden tasarımıdır .

SPARK dili , bileşenlerin belirtimini hem statik hem de dinamik doğrulama için uygun bir biçimde tanımlamak için sözleşmeleri kullanan Ada dilinin iyi tanımlanmış bir alt kümesinden oluşur .

SPARK83/95/2005'te sözleşmeler Ada yorumlarında kodlanmıştır ve bu nedenle herhangi bir standart Ada derleyicisi tarafından yok sayılır, ancak SPARK "Examiner" ve ilgili araçları tarafından işlenir.

SPARK 2014, aksine, sözleşmeleri ifade etmek için Ada 2012'nin yerleşik "boyut" sözdizimini kullanır ve bunları dilin özüne getirir. SPARK 2014'ün (GNATprove) ana aracı, TBMM/GCC altyapısına dayalıdır ve TBMM Ada 2012 ön ucunun neredeyse tamamını yeniden kullanır.

Teknik Genel Bakış

SPARK, Ada'nın tüm potansiyel belirsizliklerini ve güvensiz yapılarını ortadan kaldırmaya çalışırken, Ada'nın güçlü yanlarından yararlanır. SPARK programlarının tasarımı gereği açık olması amaçlanmıştır ve davranışlarının Ada derleyici seçiminden etkilenmemesi gerekir . Bu hedeflere kısmen Ada'nın daha sorunlu özelliklerinden bazılarını (sınırsız paralel görevlendirme gibi ) çıkararak ve kısmen de uygulama tasarımcısının niyetlerini ve bir programın belirli bileşenleri için gereksinimlerini kodlayan sözleşmeler getirerek ulaşılır .

Bu yaklaşımların kombinasyonu, SPARK'ın aşağıdaki tasarım hedeflerini karşılamasını sağlar:

Sözleşme örnekleri

Aşağıdaki Ada alt program belirtimini göz önünde bulundurun: 

procedure Increment (X : in out Counter_Type);

Saf Ada'da bu, değişkeni Xbir veya bin artırabilir; veya bir global sayaç ayarlayabilir Xve sayacın orijinal değerini 'de döndürebilir X; ya da kesinlikle hiçbir şey yapmayabilir X.

SPARK 2014 ile, bir alt programın gerçekte ne yaptığına ilişkin ek bilgi sağlamak için koda sözleşmeler eklenir. Örneğin, yukarıdaki belirtimi şu şekilde değiştirebiliriz: 

procedure Increment (X : in out Counter_Type)
  with Global => null,
       Depends => (X => X);

O Bu belirtir Incrementprosedür yeni değer hesaplamasında kullanılan tek veri öğesi olduğunu (ne güncelleştirme ne de okuyun) kullanan küresel değişken ve yok Xolduğunu Xkendisi.

Alternatif olarak, tasarımcı şunları belirtebilir: 

procedure Increment (X : in out Counter_Type)
  with Global  => (In_Out => Count),
       Depends => (Count  => (Count, X),
                   X      => null);

Bu belirtir Incrementküresel değişkeni kullanacağız Countaynı pakette Incrementarasında ihraç değeri o, Countithal değerlerine bağlıdır Countve Xve ihraç değeri o Xhiç bir değişkenlere bağlı değildir ve sürekli veri sadece elde edilecektir .

GNATprove daha sonra bir alt programın spesifikasyonu ve karşılık gelen gövdesi üzerinde çalıştırılırsa, bilgi akışının bir modelini oluşturmak için alt programın gövdesini analiz eder. Bu model daha sonra ek açıklamalar ve kullanıcıya bildirilen herhangi bir tutarsızlık tarafından belirtilenle karşılaştırılır.

Bu özellikler, bir alt program çağrıldığında ( ön koşullar ) tutulması gereken veya alt programın yürütülmesi tamamlandığında ( son koşullar ) tutulacak olan çeşitli özellikler ileri sürülerek daha da genişletilebilir . Örneğin, şunları söyleyebiliriz: 

procedure Increment (X : in out Counter_Type)
  with Global  => null,
       Depends => (X => X),
       Pre     => X < Counter_Type'Last,
       Post    => X = X'Old + 1;

Bu, şimdi, yalnızca Xkendisinden türetileni değil, aynı zamanda önce Incrementçağrılannın Xtürünün son olası değerinden kesinlikle daha az olması gerektiğini ve daha sonra artı birin Xbaşlangıç ​​değerine eşit olacağını belirtir X.

Doğrulama koşulları

GNATprove ayrıca bir dizi doğrulama koşulu veya VC'ler de oluşturabilir . Bu koşullar, belirli özelliklerin belirli bir alt program için geçerli olup olmadığını belirlemek için kullanılır. En azından, GNATprove, tüm çalışma zamanı hatalarının bir alt program içinde oluşamayacağını belirlemek için VC'ler üretecektir, örneğin:

  • dizi dizini aralık dışında
  • tür aralığı ihlali
  • sıfıra bölüm
  • sayısal taşma

Bir alt programa bir son koşul veya başka bir onay eklenirse, GNATprove ayrıca, kullanıcının bu özelliklerin alt program boyunca tüm olası yollar için geçerli olduğunu göstermesini gerektiren VC'ler de üretecektir.

Kaputun altında, GNATprove, VC'leri boşaltmak için Why3 ara dili ve VC Generator ile CVC4, Z3 ve Alt-Ergo teoremi kanıtlayıcılarını kullanır. Why3 araç setinin diğer bileşenleri aracılığıyla diğer kanıtlayıcıların (etkileşimli kanıt denetleyicileri dahil) kullanımı da mümkündür.

Tarih

SPARK'ın ilk versiyonu (Ada 83'e dayalı), Southampton Üniversitesi'nde (İngiltere Savunma Bakanlığı sponsorluğunda) Bernard Carré ve Trevor Jennings tarafından üretildi . SPARK adı , Pascal programlama dilinin SPADE alt kümesine atıfta bulunarak SPADE Ada Kernel'den türetilmiştir .

Daha sonra dil, önce Program Validation Limited ve ardından Praxis Critical Systems Limited tarafından aşamalı olarak genişletildi ve geliştirildi. 2004 yılında Praxis Critical Systems Limited, adını Praxis High Integrity Systems Limited olarak değiştirdi. Ocak 2010'da şirket Altran Praxis oldu .

2009'un başlarında Praxis, AdaCore ile bir ortaklık kurdu ve GPL koşulları altında "SPARK Pro"yu piyasaya sürdü. Bunu Haziran 2009'da FOSS ve akademik topluluklara yönelik SPARK GPL Edition 2009 izledi .

Haziran 2010'da Altran-Praxis , 2015 yılında tamamlanması beklenen ABD Lunar projesi CubeSat'ın yazılımında SPARK programlama dilinin kullanılacağını duyurdu .

Ocak 2013'te Altran-Praxis adını Altran olarak değiştirdi.

SPARK 2014'ün ilk Pro sürümü 30 Nisan 2014'te duyuruldu ve hemen ardından FLOSS ve akademik toplulukları hedefleyen SPARK 2014 GPL sürümü geldi .

Endüstriyel uygulamalar

Güvenlikle ilgili sistemler

SPARK, ticari havacılık ( Rolls-Royce Trent serisi jet motorları, ARINC ACAMS sistemi, Lockheed Martin C130J), askeri havacılık ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), hava -trafik yönetimi (UK NATS iFACTS sistemi), demiryolu (çok sayıda sinyal uygulaması), medikal (LifeFlow ventriküler destek cihazı ) ve uzay uygulamaları ( Vermont Technical College CubeSat projesi ).

Güvenlikle ilgili sistemler

SPARK, güvenli sistem geliştirmede de kullanılmıştır. Kullanıcılar arasında Rockwell Collins (Turnstile ve SecureOne etki alanları arası çözümler), orijinal MULTOS CA'nın geliştirilmesi, NSA Tokeneer göstericisi, secunet çok seviyeli iş istasyonu, Muen ayırma çekirdeği ve Genode blok-cihaz şifreleyici yer alıyor.

Ağustos 2010'da, Altran Praxis'in baş mühendisi Rod Chapman, SPARK'ta SHA-3 adaylarından biri olan Skein'i uyguladı . SPARK ve C uygulamalarının performansını karşılaştırırken ve dikkatli optimizasyondan sonra, SPARK versiyonunun C'den sadece %5 ila %10 daha yavaş çalışmasını sağladı. Daha sonra GCC'de Ada orta uçta iyileştirme (AdaCore'dan Eric Botcazou tarafından uygulandı) ) performansta C ile tam olarak eşleşen SPARK koduyla boşluğu kapattı.

NVIDIA, güvenlik açısından kritik ürün yazılımının uygulanması için SPARK'ı da benimsemiştir.

2020'de Rod Chapman, TweetNaCl şifreleme kitaplığını SPARK 2014'te yeniden uyguladı. Kitaplığın SPARK sürümü, tam otomatik etkin tip güvenliği, bellek güvenliği ve bazı doğruluk özellikleri kanıtına sahiptir ve baştan sona sabit zamanlı algoritmaları korur. SPARK kodu ayrıca TweetNaCl'den önemli ölçüde daha hızlıdır.

Ayrıca bakınız

Referanslar

daha fazla okuma

Dış bağlantılar