Bug#617551: ITP: spark -- SPARK programming language tools
9 березня 2011 о 18:49 + Florian Schanda написав(-ла): > I would say "This package contains the tools necessary for checking > if programs adhere to the SPARK rules and the tools to show freedom > of runtime exceptions in those programs." > > And then also say: "To compile SPARK programs use any standards-compliant > Ada compiler, such as GNAT." Thanks, I'll use this description. signature.asc Description: Digital signature
Bug#617551: ITP: spark -- SPARK programming language tools
10 березня 2011 о 09:48 +0100 Bernhard R. Link написав(-ла): > * Євгеній Мещеряков [110309 19:39]: > > Description : SPARK programming language toolset > > > > SPARK is a programming language and a set of software development > > products for high assurance software. The SPARK programming language is > > the only language specifically designed to support the development of > > safety or security critical software. In combination with the SPARK > > toolset, SPARK prevents, detects and eliminates defects early in the > > lifecycle as the source code is developed. It is, effectively, the > > result of applying the principles of Correctness by Construction to the > > design of a programming language and associated verification tools. > > I suggest to either replace that or simply remove it. At least I'm not > able to get any information out of it. > Does this text look better (from Wikipedia): SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety or for business integrity. signature.asc Description: Digital signature
Bug#617551: ITP: spark -- SPARK programming language tools
Євгеній Мещеряков wrote: > SPARK is a programming language and a set of software development > products for high assurance software. The SPARK programming language > is the only language specifically designed to support the development > of safety or security critical software. In combination with the SPARK > toolset, SPARK prevents, detects and eliminates defects early in the > lifecycle as the source code is developed. It is, effectively, the > result of applying the principles of Correctness by Construction to > the design of a programming language and associated verification > tools. > > This package contains tools for verification of programs written in > SPARK. To compile SPARK programs use Ada compiller available in > package 'gnat'. I would say "This package contains the tools necessary for checking if programs adhere to the SPARK rules and the tools to show freedom of runtime exceptions in those programs." And then also say: "To compile SPARK programs use any standards-compliant Ada compiler, such as GNAT." (One of the design principles of SPARK was to have an unambigous subset of Ada so that one is not tied to a particular compiler and that reasoning about it is sound.) Florian This email is confidential and intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient, be advised that you have received this email in error and that any use, disclosure, copying or distribution or any action taken or omitted to be taken in reliance on it is strictly prohibited. If you have received this email in error please contact the sender. Any views or opinions presented in this email are solely those of the author and do not necessarily represent those of Altran Praxis. Although this email and any attachments are believed to be free of any virus or other defect, no responsibility is accepted by Altran Praxis or any of its associated companies for any loss or damage arising in any way from the receipt or use thereof. The IT Department at Altran Praxis can be contacted at it.supp...@altran-praxis.com. Altran Praxis Ltd: Company Number: 3302507, registered in England and Wales Registered Address: 20 Manvers Street, Bath. BA1 1PX VAT Registered in Great Britain: 682635707
Bug#617551: ITP: spark -- SPARK programming language tools
Package: wnpp Severity: wishlist Owner: "Євгеній Мещеряков" * Package name: spark Version : spark-gpl-2010-SMT * URL : http://libre.adacore.com/libre/tools/spark-gpl-edition/ * License : GPL3+ Programming Lang: Ada, Prolog, C++ Description : SPARK programming language toolset SPARK is a programming language and a set of software development products for high assurance software. The SPARK programming language is the only language specifically designed to support the development of safety or security critical software. In combination with the SPARK toolset, SPARK prevents, detects and eliminates defects early in the lifecycle as the source code is developed. It is, effectively, the result of applying the principles of Correctness by Construction to the design of a programming language and associated verification tools. This package contains tools for verification of programs written in SPARK. To compile SPARK programs use Ada compiller available in package 'gnat'. --- The description is stolen from the upstream homepage (http://altran-praxis.com/spark.aspx). Corrections/improvements are welcome. -- To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/20110309183721.18894.83636.report...@openfonts.org
Bug#617551: ITP: spark -- SPARK programming language tools
* Євгеній Мещеряков [110309 19:39]: > Description : SPARK programming language toolset > > SPARK is a programming language and a set of software development > products for high assurance software. The SPARK programming language is > the only language specifically designed to support the development of > safety or security critical software. In combination with the SPARK > toolset, SPARK prevents, detects and eliminates defects early in the > lifecycle as the source code is developed. It is, effectively, the > result of applying the principles of Correctness by Construction to the > design of a programming language and associated verification tools. I suggest to either replace that or simply remove it. At least I'm not able to get any information out of it. > This package contains tools for verification of programs written in > SPARK. To compile SPARK programs use Ada compiller available in package > 'gnat'. s/in SPARK/in the programing language SPARK/ and that says much more than all the previous marketing blurb. Bernhard R. Link -- To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/20110310084847.ga19...@pcpool00.mathematik.uni-freiburg.de
