Spec Sharp

本来の表記は「Spec#」です。この記事に付けられたページ名は技術的な制限または記事名の制約により不正確なものとなっています。
Spec#
パラダイム マルチパラダイム: 構造化, 命令型, オブジェクト指向, イベント駆動, 関数型, 契約
登場時期 2004年 (20年前) (2004)
設計者 Microsoft Research
開発者 Microsoft Research
最新リリース SpecSharp 2011-10-03/ 2011年10月7日 (13年前) (2011-10-07)
型付け 静的型付け, 強い型付け, 安全, 公称的派生型
影響を受けた言語 C#, Eiffel
影響を与えた言語 Sing#
ウェブサイト research.microsoft.com/specsharp/
テンプレートを表示

Spec#とは、C#にEiffel風の仕様記述言語的要素を追加したプログラミング言語である。Spec#ではオブジェクト不変条件・事前条件・事後条件などの契約を記述するための構文を持つ。ESC/Javaのように、定理証明機を用いた静的検証ツールを持っており、不変条件の多くを静的に検証できる。

.NET Framework 4.0におけるコードコントラクトAPIはSpec#とともに発展してきた。 Spec#はSing#の基礎にもなっている。

特徴

C#と比べ、Spec#には以下の要素を持つ。

  • null非許容参照型
  • 事前条件・事後条件を書くための構文
  • Java風の検査例外
  • 簡易構文

例

事前条件・事後条件・null非許容参照型を用いた例を以下に示す。(ブラウザ上でSpec#を試す) 

static int Main(string![] args)
    requires args.Length > 0;
    ensures return == 0;
{
    foreach(string arg in args)
    {
        Console.WriteLine(arg);
    }
    return 0;
}
  • ! はnull非許容参照型である。argsはnullであってはいけない。
  • requires は事前条件である。この例ではargsの数が0以下であることは許されない。
  • ensures 事後条件である。Main関数は0を返さなければならない。

Sing#

Sing#はMicrosoft ResearchがSingularity(OS)を開発するためにSpec#を拡張した言語である。Sing#では低水準プログラミング言語におけるチャネルと契約を扱える。

脚注

[脚注の使い方]

出典

  • Barnett, M., K. R. M. Leino, W. Schulte, "The Spec# Programming System: An Overview." Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), Marseilles. Springer-Verlag, 2004.

関連項目

外部リンク

アーキテクチャ
共通言語基盤
言語
パッケージマネージャ
関連技術
その他のCLI実装
組織
開発環境
その他
カテゴリ カテゴリ

Read other articles:

Bahasa Võro

Cari artikel bahasa  Cari berdasarkan kode ISO 639 (Uji coba)  Kolom pencarian ini hanya didukung oleh beberapa antarmuka Halaman bahasa acak Bahasa Võro võro kiilʼ Dituturkan diEstoniaWilayahEstonia selatanEtnisVõrosPenutur87, termasuk Seto (2011)[1] Rincian data penutur Jumlah penutur beserta (jika ada) metode pengambilan, jenis, tanggal, dan tempat. 74.499 (2011) Rumpun bahasaUralik FinikEstonia SelatanVõro Aspek ketatabahasaanTipologibahasa aglutinatifSubj...

 

Abdul Qayum Sher

Pakistani Army officer and War Hero This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Abdul Qayum Sher – news · newspapers · books · scholar · JSTOR (February 2022) (Learn how and when to remove this template message) BrigadierAbdul Qayum SherHJBorn(1919-05-15)15 May 1919Jangal Khel, Kohat, NWFP, British India...

 

An Education

An EducationPoster film An EducationSutradaraLone ScherfigProduserFinola DwyerAmanda PoseyDitulis olehNick HornbyBerdasarkanAn Educationoleh Lynn BarberPemeranCarey MulliganPeter SarsgaardAlfred MolinaRosamund PikeDominic CooperEmma ThompsonOlivia WilliamsPenata musikPaul EnglishbySinematograferJohn de BormanPenyuntingBarney PillingPerusahaanproduksiBBC FilmsFinola Dwyer ProductionsWildgaze FilmsEndgame EntertainmentDistributorSony Pictures ClassicsTanggal rilis 18 Januari 2009 (20...

Piet Keizer

Dutch footballer (1943–2017) Piet Keizer Keizer in 1973Personal informationFull name Petrus Johannes KeizerDate of birth (1943-06-14)14 June 1943Place of birth Amsterdam, NetherlandsDate of death 10 February 2017(2017-02-10) (aged 73)Position(s) Left wingerYouth career1953–1955 Amstel1955–1961 AjaxSenior career*Years Team Apps (Gls)1961–1974 Ajax 365 (146)International career1962–1974 Netherlands 34 (11) Medal record Men's football Representing  Netherlands FIFA World Cup ...

 

Jura (department)

Department of France in Bourgogne-Franche-Comté For other places with the same name, see Jura (disambiguation). Not to be confused with the Swiss Republic and Canton of Jura. Department of France in Bourgogne-Franche-ComtéJuraDepartment of France From top down, left to right: Lac de Vouglans, Baume-les-Messieurs, Poligny, Lac de Bonlieu, Lac de l'Abbaye, Les Planches-près-Arbois, Chancia FlagCoat of armsLocation of Jura in FranceCoordinates: 46°40′31″N 5°33′16″E / ...

 

Lapangan Panahan Gelora Bung Karno

Lapangan Panahan Gelora Bung KarnoLapangan Panahan GBK, Lapangan Panahan SenayanInformasi stadionPemilikKementerian Sekretariat Negara Republik IndonesiaOperatorPusat Pengelolaan Kompleks Gelora Bung KarnoLokasiLokasi Gelora, Tanah Abang, Jakarta Pusat, DKI Jakarta, IndonesiaKonstruksiDibuat2016Dibuka2 November 2017Data teknisKapasitas97Situs web[1]Sunting kotak info • L • BBantuan penggunaan templat ini Lapangan Panahan Gelora Bung Karno adalah sebuah Lapangan panahan di Jakart...

Delta B

Retired American expendable rocket Delta B prior to the launch of TIROS-8FunctionExpendable launch systemCountry of originUnited StatesCapacity Payload to LEOAltitude350 nautical miles (650 km; 400 mi)Mass800 pounds (360 kg)[1]Payload to Earth escape trajectoryMass130 pounds (59 kg)[1] Launch historyStatusRetired[2]Launch sitesCape Canaveral LC-17[3]Total launches9Success(es)8Failure(s)1First flight13 December 1962Last flight19 March 1964 ...

 

Michael Oakeshott

British philosopher (1901–1990) Michael OakeshottOakeshott in the 1960sBornMichael Joseph Oakeshott(1901-12-11)11 December 1901Chelsfield, London, EnglandDied19 December 1990(1990-12-19) (aged 89)Acton, EnglandAlma materGonville and Caius College, CambridgeEra20th-century philosophyRegionWestern philosophy British philosophy SchoolBritish idealism[1]Liberal conservatism[2]Main interestsHistory of philosophyIntellectual historyHistory of political thoughtPhilosophy ...

 

Siu Lek Yuen

Siu Lek Yuen Nullah with Kwong Yuen Estate in the background in April 2008. Siu Lek Yuen in November 2016 Siu Lek Yuen Village. Siu Lek Yuen (Chinese: 小瀝源) is an area in Sha Tin District, New Territories East. Located to the east of Yuen Chau Kok, the area is surrounded on three sides by the Ma On Shan Country Park. Nowadays it is a residential area. Name The name means the origin of small river in Chinese. It is so named because the area situated originally between two rivers.[...

Wolf Creek Inn State Heritage Site

State park in Oregon, United States Wolf Creek Inn State Heritage SiteShow map of OregonShow map of the United StatesTypePublic, stateLocationJosephine County, OregonNearest cityGrants PassCoordinates42°41′43″N 123°23′46″W / 42.69515833°N 123.3959972°W / 42.69515833; -123.3959972[1]Operated byOregon Parks and Recreation DepartmentWebsitehttps://www.wolfcreekinn.comWolf Creek TavernU.S. National Register of Historic Places LocationWolf Cree...

 

Mr. Mike's Mondo Video

1979 film by Michael O'Donoghue Mr. Mike's Mondo VideoDirected byMichael O'DonoghueWritten byMichael O'DonoghueMitch GlazerDirk WittenbornEmily PragerStarringMichael O'DonoghueDan AykroydBill MurrayGilda RadnerSid ViciousCinematographyBarry ReboEdited byAlan MillerDistributed byNew Line CinemaRelease date September 21, 1979 (1979-09-21) Running time75 minutesCountryUnited StatesLanguageEnglish Mr. Mike's Mondo Video is a 1979 American comedy film conceived and directed by Satur...

 

Dornier Do 22

Torpedo bomber and maritime reconnaissance floatplane Do 22 Dornier Do 22 K in the Finnish Air Force Role Torpedo bomber and reconnaissance seaplaneType of aircraft National origin Germany Manufacturer Dornier Flugzeugwerke First flight 15 July 1938 Produced 1938–1939 Number built ~30 The Dornier Do 22 was a German seaplane, developed in the 1930s. Despite good performance, it was built only in small numbers and entirely for the export market. The type was operated in the Second World War b...

Wandegeya

Place in Central Uganda, UgandaWandegeyaWandegeyaWandegeyaMap of Kampala showing the location of Wandegeya.Coordinates: 00°19′52″N 32°34′25″E / 0.33111°N 32.57361°E / 0.33111; 32.57361Country UgandaRegionCentral UgandaDistrictKampala Capital City AuthorityDivisionKampala Central DivisionElevation1,200 m (3,900 ft)Time zoneUTC+3 (EAT) Wandegeya is a neighborhood within the city of Kampala, Uganda's capital and largest metropolitan area. The na...

 

Tytus Howard

Tytus Howard Nazionalità  Stati Uniti Peso 146 kg Football americano Ruolo Offensive tackle Squadra  Houston Texans CarrieraGiovanili 2014-2018 Alabama State HornetsSquadre di club 2019- Houston Texans Statistiche Partite 8 Partite da titolare 8 Statistiche aggiornate al 22 gennaio 2020 Modifica dati su Wikidata · Manuale Tytus Howard (Monroeville, 23 maggio 1996) è un giocatore di football americano statunitense che milita nel ruolo di offensive tackle per gli Hou...

 

William F. Varney

American politician William F. VarneyPersonal detailsBorn(1884-10-01)October 1, 1884Paterson, New Jersey, U.S.DiedDecember 13, 1960(1960-12-13) (aged 76)East Rockaway, New York, U.S.Political partyProhibitionSpouseLeonia AbramsChildren3ParentWilliam Frederick Varney (father) William Frederick Varney (October 1, 1884 – December 13, 1960) was an American politician who served as the Prohibition Party's presidential candidate in 1928 and in other New York campaigns. Life On October 1, 188...

ヨハネス12世 (ローマ教皇)

ヨハネス12世 第130代 ローマ教皇 教皇就任 955年12月16日教皇離任 964年5月14日先代 アガペトゥス2世次代 レオ8世個人情報出生 937年スポレート公国（中部イタリア）スポレート死去 964年5月14日 教皇領、ローマ原国籍 スポレート公国親 父アルベリーコ2世（スポレート公）、母アルダその他のヨハネステンプレートを表示 ヨハネス12世（Ioannes XII、937年 - 964年5月14日）は、ロ...

 

List of international prime ministerial trips made by Theresa May

International trips made by Theresa May while Prime Minister World map highlighting the 33 countries visited by Theresa May during her premiership, as of July 2019   United Kingdom   One visit   Two visits   Three visits   Four visits   Seven or more visits This article is part of a series aboutTheresa May Political positions Electoral history MP for Maidenhead One-nation conservatism Home Secretary Home Office under Theresa May Host...

 

Honest Leadership and Open Government Act

United States lobbying law Honest Leadership and Open Government Act of 2007Other short titlesCommission to Strengthen Confidence in Congress Act of 2007Congressional Pension Accountability ActLegislative Transparency and Accountability Act of 2007Long titleAn Act to provide greater transparency in the legislative process.Acronyms (colloquial)HLOGAEnacted bythe 110th United States CongressEffectiveSeptember 14, 2007CitationsPublic law110-81Statutes at Large121 Stat. 735Codifica...

Celal İbrahim

Turkish footballer Celal İbrahim Personal informationFull name Celal İbrahimDate of birth 1889Place of birth Malatya, Ottoman EmpireDate of death 21 March 1917(1917-03-21) (aged 33)Place of death Baghdad, IraqPosition(s) Left wingbackSenior career*Years Team Apps (Gls)1905–1915 Galatasaray *Club domestic league appearances and goals Celal İbrahim (1884 – 21 March 1917) was an Ottoman footballer of Kurdish origin and one of the founders of Galatasaray. He was also known as Kürt Ce...

 

Русское собрание

«Русское Собрание» Лидер Д. П. Голицын, Н. А. Энгельгардт, М. Л. Шаховской, А. Н. Лобанов-Ростовский, Н. Н. Пешков, Н. Ф. Гейден, П. Н. Апраксин, Н. Н. Белявский Основана ноябрь 1900 года Упразднена февраль — март 1917 года, попытка возрождения предпринималась в 1918 —1919&#...