TLA
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/08/04 04:19 UTC 版)
TLA
- 三文字頭字語(Three-letter acronym/abbreviation)
- Tom Lord's Arch
- テラー空港のIATA空港コード
- トラスカラ州(メキシコの州)のISO 3166-2コード
- 南西テペワン語のISO 639-3コード
TLA+
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/10/27 14:29 UTC 版)
TLA+は、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLA+は、網羅的にテスト可能な擬似コード[4]として説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。 [5] TLAはTemporal Logic of Actionsの頭字語である。
- ^ Lamport, Leslie (January 2000). Specifying Concurrent Systems with TLA+. 173. IOS Press, Amsterdam. 183–247. ISBN 978-90-5199-459-9 2015年5月22日閲覧。
- ^ Lamport, Leslie (2014年1月15日). “TLA+2: A Preliminary Guide”. 2015年5月2日閲覧。
- ^ “Tlaplus Tools - License”. CodePlex. Microsoft, Compaq (2013年4月8日). 2015年5月10日閲覧。
- ^ a b Newcombe (2014年9月29日). “Use of Formal Methods at Amazon Web Services”. Amazon. 2015年5月8日閲覧。
- ^ Lamport, Leslie (25 January 2013). “Why We Should Build Software Like We Build Houses”. Wired (Wired) 2015年5月7日閲覧。.
- ^ Lamport, Leslie (18 June 2002). “7.1 Why Specify”. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. p. 75. ISBN 978-0-321-14306-8 . "Having to describe a design precisely often reveals problems - subtle interactions and "corner cases" that are easily overlooked."
- ^ Lamport, Leslie (2012). “How to Write a 21st Century Proof”. Journal of Fixed Point Theory and Applications 11: 43–63. doi:10.1007/s11784-012-0071-6. ISSN 1661-7738 2015年5月23日閲覧。.
- ^ Øhrstrøm, Peter; Hasle, Per (1995). “3.7 Temporal Logic and Computer Science”. Temporal Logic: From Ancient Ideas to Artificial Intelligence. Studies in Linguistics and Philosophy. 57. Springer Netherlands. pp. 344–365. doi:10.1007/978-0-585-37463-5. ISBN 978-0-7923-3586-3
- ^ Lamport. “The Writings of Leslie Lamport: Proving the Correctness of Multiprocess Programs”. 2015年5月22日閲覧。
- ^ Lamport. “The Writings of Leslie Lamport: On-the-fly Garbage Collection: an Exercise in Cooperation”. 2015年5月22日閲覧。
- ^ Lamport. “The Writings of Leslie Lamport: 'Sometime' is Sometimes 'Not Never'”. 2015年5月22日閲覧。
- ^ Lamport. “The Writings of Leslie Lamport: Specifying Concurrent Programming Modules”. 2015年5月22日閲覧。
- ^ Lamport. “The Writings of Leslie Lamport: The Temporal Logic of Actions”. 2015年5月22日閲覧。
- ^ a b Yu, Yuan; Manolios, Panagiotis; Lamport, Leslie (1999). Model checking TLA+ specifications. Lecture Notes in Computer Science. 1703. Springer-Verlag. 54–66. doi:10.1007/3-540-48153-2_6. ISBN 978-3-540-66559-5 2015年5月14日閲覧。
- ^ Lamport, Leslie (18 June 2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. ISBN 978-0-321-14306-8
- ^ Lamport, Leslie (2 January 2009). The PlusCal Algorithm Language. 5684. Springer Berlin Heidelberg. 36–60. doi:10.1007/978-3-642-03466-4_2. ISBN 978-3-642-03465-7 2015年5月10日閲覧。
- ^ a b c d Cousineau, Denis; Doligez, Damien; Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán (1 January 2012). TLA+ Proofs. Lecture Notes in Computer Science. 7436. Springer Berlin Heidelberg. 147–154. doi:10.1007/978-3-642-32759-9_14. ISBN 978-3-642-32758-2 2015年5月14日閲覧。
- ^ Lamport, Leslie (18 June 2002). “8.9.2 Machine Closure”. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. p. 112. ISBN 978-0-321-14306-8 . "We seldom want to write a specification that isn't machine closed. If we do write one, it's usually by mistake."
- ^ Lamport, Leslie (18 June 2002). “8.9.6 Temporal Logic Considered Confusing”. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. p. 116. ISBN 978-0-321-14306-8 . "Indeed, [most engineers] can get along quite well with specifications of the form (8.38) that express only safety properties and don't hide any variables."
- ^ Markus A. Kuppe (3 June 2014). Distributed TLC. TLA+ Community Event 2014, Toulouse, France.
- ^ “Unsupported TLAPS features”. TLA+ Proof System. Microsoft Research - INRIA Joint Centre. 2015年5月14日閲覧。
- ^ TLA+ Proof System
- ^ Leslie Lamport (3 April 2014). Thinking for Programmers (at 21m46s). San Francisco: Microsoft. 2015年5月14日閲覧。
- ^ Lardinois (2017年5月10日). “With Cosmos DB, Microsoft wants to build one database to rule them all”. TechCrunch. 2017年5月10日閲覧。
- ^ Leslie Lamport (10 May 2017). Foundations of Azure Cosmos DB with Dr. Leslie Lamport. Microsoft Azure. 2017年5月10日閲覧。
TLA
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/10/08 20:14 UTC 版)
詳細は「三文字頭字語」を参照 特に三文字頭字語を「TLA」と呼ぶことがある。TLAという単語自体が three-letter acronym(3文字のアクロニム)ないし three-letter abbreviation(3文字の略語)に由来するイニシャリズムの頭字語であり、TLAでもある。
※この「TLA」の解説は、「頭字語」の解説の一部です。
「TLA」を含む「頭字語」の記事については、「頭字語」の概要を参照ください。
- TLAのページへのリンク