short-paper

Resource usage contracts for .NET

Authors:

Jonathan Tapicer,

Diego Garbervetsky,

Martin RouauxAuthors Info & Claims

TOPI '11: Proceedings of the 1st Workshop on Developing Tools as Plug-ins

Page 56

https://doi.org/10.1145/1984708.1984725

Published: 28 May 2011 Publication History

Get Access

Abstract

Code Contracts [2] is a tool that allows the specification and verification of contracts (pre, post-condition, invariants) in all .NET based programming languages. Resource Contracts is an extension of this language to specify resource usage in .NET programs. The new annotations, initially focussed on dynamic memory, enable modular analysis of both memory consumption and lifetime properties. They are checked by relying on the own Code Contracts static verifier and a points-to analysis. This approach is implemented as a Visual Studio extension¹, providing facilities such us autocompletion and verification at build time.

References

[1]

V. Braberman, F Fernández, D. Garbervetsky, and S Yovine. Parametric prediction of heap memory requirements. In ISMM'08. ACM, jun 2008.

Digital Library

Google Scholar

[2]

M. Fähndrich, M. Barnett, and F. Logozzo. Embedded contract languages. In SAC 2010, pages 2103--2110. ACM, 2010.

Digital Library

Google Scholar

[3]

D. Garbervetsky, M. Rouax, and J. Tapicer. SEIF project: ResourceContracts.NET. http://lafhis.dc.uba.ar/resourcecontracts/files/report.pdf.

Google Scholar

Index Terms

Resource usage contracts for .NET
1. General and reference
  1. Cross-computing tools and techniques
    1. Reliability
    2. Validation
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Liquidate your assets: reasoning about resource usage in liquid Haskell

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program ...
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
Expressing and Verifying Business Contracts with Abductive Logic Programming

SCIFF is a declarative language, based on abductive logic programming, that accommodates forward rules, predicate definitions, and constraints over finite domain variables. Its abductive declarative semantics can be related to that of deontic operators; ...

Comments

Information & Contributors

Information

Published In

TOPI '11: Proceedings of the 1st Workshop on Developing Tools as Plug-ins

May 2011

70 pages

ISBN:9781450305990

DOI:10.1145/1984708

Program Chairs:
Judith Bishop
Microsoft Research, USA
,
Karin Breitman
PUC-RIO, Brazil
,
David Notkin
University of Washington, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 May 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Conference

ICSE11

Sponsor:

SIGSOFT

ICSE11: International Conference on Software Engineering

May 28, 2011

HI, Waikiki, Honolulu, USA

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
55
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Index Terms

Recommendations

Liquidate your assets: reasoning about resource usage in liquid Haskell

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Expressing and Verifying Business Contracts with Abductive Logic Programming

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations