VCC programý

Eþzamanlý C programlarý için mekanik doðrulayýcýyýdýr. VCC eþzamanlý C programlarý için mekanik bir doðrulayýcýyý olmak için geliþtirilmiþtir. VCC bir C programý, fonksiyon özellikleri, veri deðiþmezler döngü deðiþmezler ve hayalet kod açýklamalý alýr ve bu açýklamalarý doðru kanýtlamaya çalýþýr. Eðer baþarýlý olursa, VCC program aslýnda kendi özelliklerine uygun olduðunu vaat ediyor. Iþ akýþý aþaðýdaki þekilde gösterilmiþtir. Hem de size bunun iþe yaradýðýný düþünüyorum programýnýz ne yapmak gerekiyordu ve (bazý yönlerini) tarif sözleþme ile C kodu açýklama baþlar. Sözleþmeler C öniþlemci makrolarý kullanýlarak yazýlýr, böylece, tek bir öniþlemci anahtarý kullanarak onlardan kurtulmak ve favori C derleyicisi kullanarak kod derleme. Açýklamalý programlarýnýn geçerliliðini kontrol etmek için otomatik bir teoremi prover (Z3) iletir Boogie aracýný kullanarak mantýksal formüller çevrilir. VCC öncelikle F # uygulanan ve bir eklenti modelini destekler.

Gerekenler:

· F # Runtime 2.0
· NET Framework

Kullanacaðýnýz yazýlýmlarý yasal þekilde kullanmaya özen gösteriniz. Bunun dýþýndaki hiç bir kullaným þeklini desteklemiyoruz.