dijkstracula / irving

there's no checking like bounded model checking
GNU Affero General Public License v3.0
1 stars 0 forks source link

Module instantiations should construct a factory object #58

Open dijkstracula opened 1 year ago

dijkstracula commented 1 year ago

Currently, we extract an Ivy statement that declares an instantiation of a module such as

instance file : vector(byte)
instance net: tcp.net(msg_t)

to a subclass of the backing Java object:

class file extends net.dijkstracula.melina.stdlib.vector<Long> {}
class net extends net.dijkstracula.melina.stdlib.net<IvyObj_msg_t> {}

In particular, the argument to the module is always currently translated into a type parameter.

Unfortunately this is clearly the wrong thing to do with net and probably also not the right thing with vector, since we need to initialize program state within net (in particular, the backing array of Sockets).

So, this should probably simply construct an object that behaves like a Factory instead.

VectorFactory<Long> file = new VectorFactory<Long>(); // Stateless: file.empty() produces a Vector, etc...?
Network<IvyObj_msg_t> net = new Network(); // Stateful: net.dial(42) sets up an internal routing table for pid 42
dijkstracula commented 1 year ago

This is also true of classes.

I actually wonder if the thing we need to do is make this true for all user-defined types (the remaining ones being enums and (parameterized) processes?)