CALM design - format of content of library files AND ALM library

[zhangyuanlin]

Is it a set of modules?

[Topology]

The BAT is specified by modules. A theory is a collection of modules. A library is a collection of theories. I think they are just ways of specifying different grouping of modules to create different BATs.

The question is, what are the logical units that are "whole"?

In an imperative language like java, files correspond to classes. In every file there is a "primary" class that is named the same as the file name. Within the file it is possible to define private and public sub-classes, but the common practice is that you would rarely use a nested class without needing to use the primary class as well. The jar file is a zip archive containing multiple classes that all cooperate together to provide a system or whole in terms of capability or functionality. A single class is usually a part that is not complete without others.

In ALM, what are the "natural" abstractions? We can flatten all modules into a single module, but then it becomes a headache (for humans) to reason about everything mixed together. We can break every single axiom and sort into its own module, but then the concept of module is meaningless. A module should encapsulate the axioms that are tightly related to the sorts that were introduced by the module. A module should only introduce a small number of related sorts to the hierarchy. There is some notion of orthogonality between modules, or complementary interaction. A module then is an encapsulation of capability that maximizes the possible reuse of the logical units it contains. But a module by itself does not imply a "whole". The sense of "whole" within ALM feels like it comes it at the level of a theory. A theory is likely to have a primary module with auxiliary support modules defined in order to complete the whole.

The analogy between ALM and JAVA from an organizational standpoint might look like this:

ALM <=> Java Module <=> Class Theory <=> Class File (has primary class) Library <=> Jar File

A large Java application will use many jar files to coordinate and orchestrate orthogonal functionality into a larger systemic whole. Similarly a large ALM system description might pull together modules from multiple libraries and build on them to orchestrate a more complex transition diagram.

In an object oriented language like Java, the abstract algebra is very clear. Objects have types, interfaces, can contain each other, and are manipulated in well defined ways. The abstract algebra in ALM is far less obvious. Whereas the state of objects in java are internal to the object, all state in ALM is external to instances of sorts, stored in assignments to functions, essentially relational database tables. Modules then become the primary means of grouping pieces of state together into logical chunks. While the state introduced by different modules are technically orthogonal, they do not introduce the same functions, they may not be semantically orthogonal if one module depends on another or there are state constraints in one module that are about the states defined in another module.

I think the abstraction of a theory is the first place where we can say that the state introduced by module X has no relationship to the state introduced by module Y. If it is true there is no dependency between them, and they are whole, then they belong in separate theories.

Similarly if two theories are completely independent of each other, they have no shared dependencies and they are semantically about different conceptual domains then they belong in separate libraries.

[Topology]

Theory A is whole with respect to state, sort hierarchy, axioms, etc. Theory B can be dependent on A. Theory C can be dependent on A. Theory B and Theory C are separate theories because the intersection of (B-A) and (C-A) is empty. B is whole (including A), C is whole (including A), and A is whole unto itself.

Libraries would have the same kind of relationship to each other. To make a semi concrete example. A library related to computer networking might contain all the theories about network protocols and network state necessary to model arbitrary network domains. A library for a network device X would include relevant theories of particular network protocols from the network library and extend it with device internal state. A library for network device Y would include perhaps a possibly different set of protocols and extend them with device states for Y. A system description for a network containing both types of devices would include all three libraries.

[zhangyuanlin]

Thanks! If we use Java as a template (which is alright but I think ALM does have sth - e.g., relation among objects - special, which might be the down side you mentioned above but should be a new phenomenon to study/understand), this may be better fit: ALM Java Module <=> Class Theory <=> package Library <=> library

Here is a precise/technical definition on concepts in ALM 1) A module is as defined 2) A theory is a set of modules/theories. (following Java package) 3) A library is a set of theories. (So, there is no real difference between library and theory by definition. The difference is that library is for communication purpose or convenience. But there is not implication for implementation.) In fact, ALM makes it clear that a "user program - system description" should use a theory while Java encourages a user program to be organized as a package (unnamed space is used if no package is specified) .

--- for long term, we can design theory (library) in the form of packages ---

for short term, here is a design candidate

principle: good design but extremely easy to implement. 
------ 1. we allow only one  level of theory (library) e.g., test1, test2, ...  
          use: in each import statement, people can import one such theory or a module of this theory
                  however, people not allowed to use structure such as 
                 alm.test1 (although ok in future) - i.e., we don't introduce 
                  sub-theory (sub-package in Java) for now. 
------ 2. we do need the notion of file with format 

    theory xxx % modules below belong to xxx. Future: A theory is the set of 
                       % all modules (in all files) defined for it.
        modules ....

       Here we further assume one theory is defined in one file to simply implementation 
------ 3. limitation reminder 
ideally, we give clear error message when people try to use "more advanced features".