the proceedings contain 3 papers. the special focus in this conference is on logic-basedmethods in programmingenvironments. the topics include: logic-based LSC Consistency Checking;Towards Parameterized Regular Type...
the proceedings contain 3 papers. the special focus in this conference is on logic-basedmethods in programmingenvironments. the topics include: logic-based LSC Consistency Checking;Towards Parameterized Regular Type Inference Using Set Constraints and the Full Abstraction Problem for Higher Order Functional-logic Programs.
Developing suitable formal semantics can be of great help in the understanding, design and implementation of a programming language, and act as a guide for software development tools like analyzers or partial evaluato...
详细信息
Developing suitable formal semantics can be of great help in the understanding, design and implementation of a programming language, and act as a guide for software development tools like analyzers or partial evaluators. In this sense, full abstraction is a highly desirable property, indicating a perfect correspondence between the semantics and the observable behavior of program pieces. In this work we address the question of full abstraction for the family of modern functional logic languages, in which functions can be higher order and non-deterministic, and where the semantics adopted for non-determinism is call-time choice. We show that, with respect to natural notions of observation, any semantics based on extensional functions is necessarily unsound;in contrast, we show that the higher order version of CRWL, a well-known existing semantic framework for functional logicprogramming, based on an intensional view of functions, turns out to be fully abstract and compositional.
Live sequence charts (LSCs) have been proposed as an inter- object scenario-based specification and visual programming language for reactive systems. In this paper, we introduce a logic-based framework to check the co...
详细信息
Live sequence charts (LSCs) have been proposed as an inter- object scenario-based specification and visual programming language for reactive systems. In this paper, we introduce a logic-based framework to check the consistency of an LSC specification. An LSC simulator has been implemented in logicprogramming, utilizing a memoized depth-first search strategy, to show how a reactive system in LSCs would response to a set of external event sequences. A formal notation is defined to specify external event sequences, extending the regular expression with a parallel operator and a testing control. the parallel operator allows interleaved parallel external events to be tested in LSCs simultaneously;while the testing control provides users to a new approach to specify and test certain temporal properties (e.g., CTL formula) in a form of LSC. Our framework further provides either a state transition graph or a failure trace to justify the consistency checking results.
暂无评论