Browse All Reviews
Theory Of Computation (F)
Logics And Meanings Of Programs (F.3)
Specifying And Verifying And Reasoning About Programs (F.3.1)
> Pre- And Post-Conditions (F.3.1...)
All Media Types
1-10 of 17 Reviews about "
Pre- And Post-Conditions (F.3.1...)
Dependent type theory for verification of information flow and access control policies
Nanevski A., Banerjee A., Garg D. ACM Transactions on Programming Languages and Systems 35(2): 1-41, 2013. Type: Article
Security issues are a growing concern in an increasingly connected society. Given the central role played by programming languages in the implementation of information technology systems, introducing such matters early in the specification phase o...
Sep 5 2013
Sequential dynamic logic
Bochman A., Gabbay D. Journal of Logic, Language and Information 21(3): 279-298, 2012. Type: Article
Propositional dynamic logic (PDL) is tailored to modeling and reasoning about evolving universes, such as computer programs whose states change during their execution. It is based on modal operators, such as in the formula [
Nov 19 2012
How good is your comment? A study of comments in Java programs
Haouari D., Sahraoui H., Langlais P. ESEM 2011 (Proceedings of the 2011 International Symposium on Empirical Software Engineering and Measurement, Banff, Alberta, Canada, Sep 22-23, 2011) 137-146, 2011. Type: Proceedings
To understand how developers comment, the Java code for three open-source projects was analyzed. Assuming a comment precedes the relevant program construct, an automatic analysis found that abstract methods, class declarations, interface declarati...
Jun 22 2012
A calculus of atomic actions
Elmas T., Qadeer S., Tasiran S. POPL 2009 (Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Savannah, GA, Jan 21-23, 2009) 2-15, 2008. Type: Proceedings
Verification of partial correctness of shared-variable parallel programs is a very old subject. Nearly 35 years ago, Owicki and Gries proposed the first axiomatization of partial verification of parallel programs, using Hoare-style logic . This...
Mar 16 2009
Termination analysis of logic programs through combination of type-based norms
Bruynooghe M., Codish M., Gallagher J., Genaim S., Vanhoof W. ACM Transactions on Programming Languages and Systems 29(2): 10-es, 2007. Type: Article
Establishing that all computations terminate is a fundamental, though generally undecidable, property of computer programs. Therefore, termination analyses that approximate this property have been developed for different programming languages....
Aug 29 2007
Method redefinition: ensuring alternative behaviors
Nunes I. Information Processing Letters 92(6): 279-285, 2004. Type: Article
This paper is concerned with mechanisms for preserving the behavioral properties of subclasses that redefine methods of superclasses. It explores the various mechanisms suggested in the literature, and brings out their limitations. The explored ap...
Apr 27 2005
Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results
Bultan T., Gerber R., Pugh W. ACM Transactions on Programming Languages and Systems 21(4): 747-789, 1999. Type: Article
The authors discuss the automatic analysis and verification of concurrent programs with unbounded integer variables. These programs are expressed in the event-action language and have their semantics defined in terms of infinite (because of unboun...
Mar 1 2000
Disjunctive program analysis for algebraic data types
Jensen T. ACM Transactions on Programming Languages and Systems 19(5): 751-803, 1997. Type: Article
Jensen presents a framework for analyzing uniform program properties (relating to the content of data structures rather than to the structures themselves) in a high-order functional language with recursive data structures. The development starts f...
Jun 1 1998
Lightweight closure conversion
Steckler P., Wand M. ACM Transactions on Programming Languages and Systems 19(1): 48-86, 1997. Type: Article
In order to enable a compiler to emit fast code, the authors annotate source programs with propositions during a program analysis phase. These propositions later justify certain transformations. While this is a manageable task in the analysis of c...
Dec 1 1997
The formal semantics of programming languages
Winskel G., MIT Press, Cambridge, MA, 1993.Type: Book (9780262231695)
The mathematics, techniques, and concepts of operational, denotational, and axiomatic semantics are presented. This introductory book is primarily addressed to undergraduate and graduate students, so it starts with basic material. But more advance...
Aug 1 1994
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.