A magnetization mapping approach for passive shim design in MRI

A new passive shim design method is presented which is based on a magnetization mapping approach. Well defined regions with similar magnetization values define the optimal number of passive shims, their shape and position. The new design method is applied in a shimming process without prior-axial shim localization; this reduces the possibility of introducing new errors. The new shim design methodology reduces the number of iterations and the quantity of material required to shim a magnet. Only a few iterations (1-5) are required to shim a whole body horizontal bore magnet with a manufacturing error tolerance larger than 0.1 mm and smaller than 0.5 mm. One numerical example is presented

Tool support for generating passive C++ test oracles from object-z specifications

A test oracle provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. We describe the "Warlock" prototype tool that supports the method. Warlock is built on top of an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.