{"id":{"repo_id":"ucf","oai_identifier":"oai:stars.library.ucf.edu:etd-2173"},"canonical_url":"https://search.dev.ndltd.org/etd/ucf/oai:stars.library.ucf.edu:etd-2173","repository":{"repo_id":"ucf","name":"Central Florida","base_url":"https://stars.library.ucf.edu/do/oai/"},"display":{"title":"Reasoning Tradeoffs in Implicit Invocation and Aspect Oriented Languages","abstract":"To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used. This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable.","abstract_html":"To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used. This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable.","abstract_has_math":false,"creators":["Sanchez Salazar, Jose"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Leavens, Gary"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-01-01T08:00:00Z","date_published":"2015-01-01T08:00:00Z","updated_at":"2026-07-24T05:09:50Z","subjects":["Program reasoning","static verification","implicit invocation","aspect orientation","ptolemy language","jml","events","Computer Sciences","Engineering"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["CFE0005706"],"render_values":[{"text":"CFE0005706","href":null,"code":true}]}]},"links":{"outbound_url":"https://stars.library.ucf.edu/etd/1174","outbound_label":"Repository record","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Leavens, Gary"]},{"key":"dc:creator","label":"Author","values":["Sanchez Salazar, Jose"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["Doctoral Dissertation (Open Access)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Program reasoning","static verification","implicit invocation","aspect orientation","ptolemy language","jml","events","Computer Sciences","Engineering"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["CFE0005706"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://stars.library.ucf.edu/etd/1174"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["<p>If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at <a href=\"mailto:STARS@ucf.edu\">STARS@ucf.edu</a></p>","Doctor of Philosophy (Ph.D.)","College of Engineering and Computer Science","Computer Science"]},{"key":"dc:description.abstract","label":"Abstract","values":["To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used. This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Reasoning Tradeoffs in Implicit Invocation and Aspect Oriented Languages"]}]}],"canonical_facts":{"dc:contributor":["Leavens, Gary"],"dc:creator":["Sanchez Salazar, Jose"],"dc:description":["<p>If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at <a href=\"mailto:STARS@ucf.edu\">STARS@ucf.edu</a></p>","Doctor of Philosophy (Ph.D.)","College of Engineering and Computer Science","Computer Science"],"dc:description.abstract":["To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used. This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable."],"dc:format":["application/pdf"],"dc:identifier":["CFE0005706"],"dc:identifier.uri":["https://stars.library.ucf.edu/etd/1174"],"dc:language":["English"],"dc:subject":["Program reasoning","static verification","implicit invocation","aspect orientation","ptolemy language","jml","events","Computer Sciences","Engineering"],"dc:title":["Reasoning Tradeoffs in Implicit Invocation and Aspect Oriented Languages"],"dc:type":["Doctoral Dissertation (Open Access)"]},"updated_at":"2026-07-24T05:09:50Z"}