Teaching skills for problem solving is usually accomplished on the basis of good examples of problems and corresponding sound solutions. By studying well-constructed examples the student learns how to analyze and decompose non-elementary problems and learns how to provide well-organized solutions.The tools we demonstrate support the teacher in presenting problems in an effective way and help the student in solving them. The teacher chooses a problem and provides a solution within Access or Excel, usually reducing the original problem to a collection of simpler, logically related sub-problems. The system thoroughly analyzes the teacher's solution and provides feedback about its structure as well as many automatically generated solution hints for the student. The teacher may add his own suggestions and establishes the form and content of the problem's presentation. Essentially, the teacher can specify which aspects of his own solution should be visible to the student. In this way, the difficulties for the student to solve the task can be largely controlled.The problem is proposed as a (possibly incomplete) set of sub-problems whose mutual relations may be left partially unspecified. In the same vein, some of the suggestions may be hidden in the initial problem presentation. The student can ask for hints during his solution attempts, and receives them at the price of penalties in the final evaluation. The results that the teacher's solution produces for the different sub-problems are supplied to the student (just the results, not the solutions). This provides three main benefits. The first one is motivational: the teacher's result is a clearly visible goal to reproduce and, by simple comparison, provides immediate feedback about the correctness of the student's solution attempts. The second benefit stems from the fact that the student is allowed to face the collection of sub-problems in a more flexible way. In fact, he can exploit the teacher's results to solve a particular sub-problem, independently from the sub-problems that he has (or has not) already solved. Finally, since the teacher's hidden solutions provide results that are assumed to be reliable, if the student uses them instead of his own results, error propagation is totally prevented.The system uses the teacher's results to automatically check the correctness of the student's results by comparison, and by considering different data samples the system infers the correctness of the student's solution. Moreover, since correctness is established by comparing results, the system will accept any solution that produces the same results as those arising from the teacher's solution, regardless of how the former are obtained. Experimentation with the system at the Italian Naval Academy has given good evidence that non-elementary problems can be proposed in a working context where students are stimulated to elaborate personal comprehension and to develop original solution techniques.The engineering of the system has been funded by the AICA-CRUI project "IT4PS - Information Technology for Problem Solving".

In Ferrucci, Pacini and Sessa (1995) an extended form of resolution, called Reduced SLD resolution (RSLD), is introduced. In essence, an RSLD derivation is an SLD derivation such that redundancy elimination from resolvents is performed after each rewriting step. It is intuitive that redundancy elimination may have positive effects on derivation process. However, undesiderable effects are also possible. In particular, as shown in this paper, program termination as well as completeness of loop checking mechanisms via a given selection rule may be lost. The study of such effects has led us to an analysis of selection rule basic concepts, so that we have found convenient to move the attention from rules of atom selection to rules of atom scheduling. A priority mechanism for atom scheduling is built, where a priority is assigned to each atom in a resolvent, and primary importance is given to the event of arrival of new atoms from the body of the applied clause at rewriting time. This new computational model proves able to address the study of redundancy elimination effects, giving at the same time interesting insights into general properties of selection rules. As a matter of fact, a class of scheduling rules, namely the specialisation independent ones, is defined in the paper by using not trivial semantic arguments. As a quite surprising result, specialisation independent scheduling rules turn out to coincide with a class of rules which have an immediate structural characterisation (named stack-queue rules). Then we prove that such scheduling rules are tolerant to redundancy elimination, in the sense that neither program termination nor completeness of equality loop check is lost passing from SLD to RSLD.

The literature offers several examples of executable specification languages, ranging from mathematically based notation to visual formalisms. In this paper, an analysis environment for executable system specifications based on the language RSF (Requirement Specification Formalism) is presented. The analysis environment also contains two other linguistic tools — RSQ (Requirement Specification Querying), and SEF (Specification Execution Filtering). Using RSQ, classes of execution paths with certain properties can be exercised, so that selected behavioral aspects can be observed. Using SEF, the amount of information and the times at which it is output can be controlled, making the behavior analysis more effective. The paper shows how the notation of RSF, with its few basic concepts, is naturally exploited as a nucleus for the other tools, which are easily integrated to produce the final analysis environment. The combination of RSQ and SEF allows the planning of testing and analysis activities. A working session is shown for a specification describing a telephone switch call handler.

A system for the definition, querying and analysis of executable specification is presented in the paper. After a short review RSF, a specification language for the definition of systems with time constraints, the authors consider the problem of querying the specifications. The query language RSQ allows one to characterize sub-classes of possible specification execution behaviours in terms of queries directed to the specification. The problem of selection of significant information produced during the execution of the specification is also considered. The system proposes three linguistic tools, one for the definition, one for the querying and the last for the filtering of executable software specifications. The linguistic tools are quite homogeneous both in their syntax and semantics and support the organization of software behaviour inspection and analysis in the RSF prototyping environment.>

Refining a specification S1 means to provide another specification S2 which contains all the information given in S1 but with more detail. In this paper, we use logical implication from lower to higher levels of logic specifications to give a definition of refinement between these levels. This guarantees that any property of the higher level is also verified at the lower one. The definition of the relation "is refinement of" is given for specifications which are general first-order theories and it is proved to be transitive. A relevant aspect is that the different levels of logic specifications are in general not immediately comparable, because they can use different vocabularies. For this reason, the concept of transcription is introduced formally in our definition. Then the particular case of Horn specifications is considered. Horn specification semantics can be given by the methodology of least models. This may suggest definitions of the concept of refinement different from the one based on logical implication from lower to higher levels. However, conceptual problems can arise depending on the kind of the refinement definition chosen. Perhaps the most interesting effect is that the property of refinement transitivity may be lost. A possible way to restore the transitivity is provided.

The availability of executable specification languages allows testing to be carried out soon after or concurrently with the requirements specification phase. In addition, it becomes possible to use these languages for rapid prototyping, making it possible to gather information on properties of the specified target system including its behavior in response to external events. The inspection of software behavior is viewed as the querying of executable specifications. A language RSQ is defined for the purpose of constructing queries against executable specifications expressed in RSF, a language for the description of systems with time constraints. A query is able to single out a subclass of possible behaviors based on properties supplied by the query. The integration of RSQ with RSF enhances the analytical abilities of the software designer and developer.>

A system to generate and interpret customized visual languages in given application areas is presented. The generation is highly automated. The user presents a set of sample visual sentences to the generator. The generator uses inference grammar techniques to produce a grammar that generalizes the initial set of sample sentences, and exploits general semantic information about the application area to determine the meaning of the visual sentences in the inferred language. The interpreter is modeled on an attribute grammar. A knowledge base, constructed during the generation of the system, is then consulted to construct the meaning of the visual sentence. The architecture of the system and its use in the application environment of visual text editing (inspired by the Heidelberg icon set) enhanced with file management features are reported.>

RSF is a formalism for specifying and prototyping systems with time constraints. Specifications are given via a set of transition rules. The application of a transition rule is dependent upon certain events. The occurrence times of the events and the data associated with them must satisfy given properties. As a consequence of the application of a rule, some events are generated and others are scheduled to occur in the future, after given intervals of time. Specifications can be queried, and the computation of answers to queries provides a generalized form of rapid prototyping. Executability is obtained by mapping the RSF rules into logic programming. The rationale, a definition of the formalism, the execution techniques which support the general notion of rapid prototyping and a few examples of its use are presented.>