Schema Disjunction Algorithm

First, convert the Exceptional Instance (e.g. Address Error) so that the "Xi" notation is substituted by the "Delta" notation. This is achived by substituting the "Xi-S" symbol with a "Delta-S" symbol and adding the axiom s=s', where s is the state schema in question (e.g. s=store).

Create the top part (signature part) of the disjoined schema (e.g. Assign) by merging the top parts of the Normal Instance(e.g Assign OK) and the Exceptional Instance (e.g. Address Error), so that each input and output variable is declared only once.

Split the bottom (axiom part) of the disjoined schema into two parts that are conected with the disjunction operator (logical OR). In the LHS part, copy the axiom part of the Normal Instance enclosed in square brackets and on the RHS copy the RHS of the exceptional schema enclosed in brackets. DO not forget that the axiom part of this schema will have an extra axiom (e.g. store=store')

Notes on Lecture 9 (full-time)

Slide 21:

"Evaluation in first-order logic"

First we write out all the possible Q predicates. Because Q={(x,y)|x=y} and x,y in {M,T,H} we get:

Q= {(Mark, Mark), (Harry, Harry), (Tom, Tom)} (1)

In our theory we are given P(a,y) (2)

and in the structure we are given a=Tom (3).

We see from the possible P pairs {(Tom, Mark), (Tom, Harry), (Mark, Harry) } (4)

that the only possible values for y from (2), (3) and (4) are:

y in {Mark,Harry} (5)

so from (4),(5) we have that:

P={(Tom,Mark),(Tom, Harry)} (6)


We need now to check whether there exists an x in {T,M,H} such that for all y in {T,M,H} Q(f(y),x) is true (our theory)

We check one by one all the allowed values of y:

For y=Mark:

Q(f(Mark), x) = Q(Harry,x)

in order for this predicate to be true, it needs to be one of the allowed predicates in (1).
The only value of x that satisfies this is x=Harry

For y=Harry

Q(f(Harry),x)=Q(Harry,x)

similarly, in order for this predicate to be true, it it needs to be one of the allowed predicates in (1).
The only value of x that satisfies this is x=Harry

Therefore, our theory, given the specific structure becomes true for x=Harry.
We say that the structure is a model for our theory.

Structure:
X={T,M,H}
a=T
P={(Tom, Mark), (Tom, Harry), (Mark, Harry) }
Q=Q={(x,y)|x=y}
f(T)=m,f(M)=f(H)=H

Notes on Lecture 7 : synchronized methods

The following notes are extracts from the Sun Java specification document. They are provided here as supplementary notes to the Singleton pattern that uses a synchronized method for ensuring that there is only a single instance of the Singleton object.

"The Java programming language provides multiple mechanisms for communicating between threads. The most basic of these methods is synchronization, which is implemented using monitors. Each object in Java is associated with a monitor, which a thread can lock or unlock. Only one thread at a time may hold a lock on a monitor. Any other threads attempting to lock that monitor are blocked until they can obtain a lock on that monitor. A thread t may lock a particular monitor multiple times; each unlock reverses the effect of one lock operation.

A synchronized method automatically performs a lock action when it is invoked; its body is not executed until the lock action has successfully completed. If the method is an instance method, it locks the monitor associated with the instance for which it was invoked (that is, the object that will be known as this during execution of the body of the method). If the method is static, it locks the monitor associated with the Class object that represents the class in which the method is defined. If execution of the method's body is ever completed, either normally or abruptly, an unlock action is automatically performed on that same monitor. "


http://java.sun.com/docs/books/jls/third_edition/html/memory.html#56318

Notes on Lecture 7 : Singleton Pattern

On the Singleton implementation shown below, there was a question on why the getSpooler() method does not seem to have a return value in the signature, although the singleton instance _spooler is returned at the end of the method implementation:

That was a typo and I have corrected it. The return type in the signature should be PrintSpooler.

There was also a question relating to declaring the constructor as "private" and whether we may have multiple constructors and whether they would all be private. We make the constructor private so an instance can only be created from within the static method of the class. Since we are only interested in having a single instance of PrintSpooler, it is rather unlikely that we would need the flexibility of having more than one constructors. Most likely we are able to define our one instance exactly and assign a single constructor to it. Certainly, the classic version of Singleton has one constructor. However, if we did have more than one constructor, they would all need to be declared "private" for the same reason.

Public class PrintSpooler {

// a prototype for a spooler class,

// such that only one instance can ever exist

private static PrintSpooler _spooler;

private PrintSpooler()

{ /* private constructor */ }

public static synchronized PrintSpooler

getSpooler() {

if (_spooler == null) _spooler = new

PrintSpooler();

return _spooler;

}

}

Rational Rose: system actors

To distinguish between a human actor and a system actor, you may use an Actor Decoration instead of an Actor Icon.

clone() in Java

Please check the following documentation for the clone() method of the Object() Class in java, re question on how it compares on object equality...

http://java.sun.com/j2se/1.4.2/docs/api/java/lang/Object.html

New Rational Rose Tutorial

Please check Blackboard->Design->Rational Rose->Tutorial 1