зеркало из https://github.com/microsoft/ivy.git
addint initializers
This commit is contained in:
Ken McMillan
Родитель
e3f0413b81
Коммит
b1438bb340
|
|
@ -6,3 +6,10 @@ account2
|
|||
account3
|
||||
leader_election_ring_repl
|
||||
udp
|
||||
leader_election_ring_udp
|
||||
leader_election_ring_udp2
|
||||
paraminit
|
||||
paraminit3
|
||||
timeout_test
|
||||
udp_test
|
||||
udp_test2
|
||||
|
|
|
|||
|
|
@ -12,4 +12,4 @@ object foo(me:t) = {
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
|
|
|||
|
|
@ -12,4 +12,4 @@ object foo(me:t) = {
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me),bit(me)
|
||||
extract iso_foo(me:t) = foo(me),bit(me)
|
||||
|
|
|
|||
|
|
@ -12,4 +12,4 @@ object foo(me:t) = {
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me),bit(me)
|
||||
extract iso_foo(me:t) = foo(me),bit(me)
|
||||
|
|
|
|||
|
|
@ -172,4 +172,4 @@ object id_impl = {
|
|||
|
||||
isolate iso_id = id with id_impl
|
||||
|
||||
extract iso_impl(me) = app(me),trans.impl(me),node_impl,id_impl,asgn
|
||||
extract iso_impl(me:node.trans) = app(me),trans.impl(me),node_impl,id_impl,asgn
|
||||
|
|
|
|||
|
|
@ -174,4 +174,4 @@ isolate iso_id = id with id_impl
|
|||
include timeout
|
||||
instance sec(X:node.t) : timeout_sec
|
||||
|
||||
extract iso_impl(me) = app(me),trans.impl(me),sec.impl(me),node_impl,id_impl,asgn
|
||||
extract iso_impl(me:node.t) = app(me),trans.impl(me),sec.impl(me),node_impl,id_impl,asgn
|
||||
|
|
|
|||
|
|
@ -10,12 +10,12 @@ unsatisfactory. Ideally, we would like a real network to take this
|
|||
role.
|
||||
|
||||
In this section, we'll see how to accomplish that. That is, we will
|
||||
implment a protocol as a collection of processes communicating over a
|
||||
implement a protocol as a collection of processes communicating over a
|
||||
network.
|
||||
|
||||
## A network interface
|
||||
|
||||
Ivy provides a simple interface to the Unix Datagram protocol (UDP) in
|
||||
Ivy provides a simple interface to the Unix Datagram Protocol (UDP) in
|
||||
a module called `udp`. Here is the interface specification:
|
||||
|
||||
module udp_simple(addr,pkt) = {
|
||||
|
|
@ -43,14 +43,14 @@ The interface is a module with two parameters: the type `addr` of
|
|||
network addresses, and the type `pkt` of packets. It has two actions,
|
||||
`recv` and `send`. These are very similar to actions of the abstract
|
||||
transport interface we used in the leader election protocol. The only
|
||||
difference is that the `send` action the source address of the packet
|
||||
as a paramater as well as the destination address. We'll see the rason
|
||||
difference is that the `send` action takes the source address of the packet
|
||||
as a parameter as well as the destination address. We'll see the reason
|
||||
for this shortly. Action `recv` is imported by the interface (meaning
|
||||
the user must implement it) while `send` is exported (meaning that the
|
||||
module implements it).
|
||||
the user must implement it) while `send` is exported (meaning that `udp_simple`
|
||||
implements it).
|
||||
|
||||
As in the leader example, the specification promises that only packets
|
||||
that have been sent wil be received (but packets may be dropped,
|
||||
that have been sent will be received (but packets may be dropped,
|
||||
duplicated or re-ordered).
|
||||
|
||||
For now, ignore the definition of object `impl`. We'll come back to it
|
||||
|
|
@ -78,7 +78,7 @@ Here, we define a type of network addresses `a` and a type of packets
|
|||
`p`. We include the `udp` module (which is part of IVy's system
|
||||
libraries). We then make an instance of `udp_simple`. To allow us to
|
||||
interact with this module, we import the `recv` action from the
|
||||
environment and export `send`. Finally, we interp the types:
|
||||
environment and export `send`. Finally, we interpret the types:
|
||||
addresses are one-bit numbers and packets are 16-bit numbers. Since
|
||||
we don't want to compile the specification, we extract just the
|
||||
implementation of the interface, which is `foo.impl`.
|
||||
|
|
@ -86,7 +86,7 @@ implementation of the interface, which is `foo.impl`.
|
|||
We compile and run this program as follows:
|
||||
|
||||
$ ivy_to_cpp target=repl isolate=iso_impl udp_test.ivy
|
||||
` $ g++ -o udp_test udp_test.cpp
|
||||
$ g++ -o udp_test udp_test.cpp
|
||||
$ ./udp_test
|
||||
>
|
||||
|
||||
|
|
@ -95,10 +95,10 @@ Now we can send a packets:
|
|||
> foo.send(0,1,2)
|
||||
> foo.recv(1,2)
|
||||
|
||||
What happend here? When we started the REPL, IVY bound addresses 0 and
|
||||
1 to two UDP port numbers. Call then ports A and B. We called
|
||||
What happened here? When we started the REPL, IVY bound addresses 0 and
|
||||
1 to two UDP port numbers. Call them ports A and B. We called
|
||||
`foo.send` to send a packet from address 0 to address 1 with content
|
||||
2. The module `foo` somehow marshalled the number 2 into a packet and
|
||||
2. The module `foo` somehow marshaled the number 2 into a packet and
|
||||
sent it out on port A. It then printed a new prompt. At this point,
|
||||
the packet was received on the port B. This caused `foo.recv` to be
|
||||
called, resulting in the print-out `foo.recv(1,2)` after the prompt.
|
||||
|
|
@ -129,7 +129,7 @@ process performing the action. This is why `send` has the parameter
|
|||
|
||||
We can extract just one process as follows:
|
||||
|
||||
extract iso_impl(me) = foo.impl(me)
|
||||
extract iso_impl(me:a) = foo.impl(me)
|
||||
|
||||
Here, `me` is a symbolic constant that represents the first parameter
|
||||
of of each action. The first parameter is "stripped" by replacing it
|
||||
|
|
@ -139,7 +139,7 @@ Before thinking about this too hard, let's just run it to see what
|
|||
happens. We compile as usual:
|
||||
|
||||
$ ivy_to_cpp target=repl isolate=iso_impl udp_test2.ivy
|
||||
` $ g++ -o udp_test2 udp_test2.cpp
|
||||
$ g++ -o udp_test2 udp_test2.cpp
|
||||
|
||||
Now, open up a new terminal that we'll call terminal A. In that
|
||||
terminal try to run `upd_test2`:
|
||||
|
|
@ -169,7 +169,7 @@ Now, let's send a packet from A to B:
|
|||
|
||||
Notice that we omit the `src` parameter of `foo.send`, since that was
|
||||
given on the command line. Similarly, when terminal B receives the
|
||||
packet, it print `foo.recv(2)`, because the first parameter `dst` is
|
||||
packet, it prints `foo.recv(2)`, because the first parameter `dst` is
|
||||
implicit.
|
||||
|
||||
We can, of course, send a packet in the opposite direction:
|
||||
|
|
@ -188,7 +188,7 @@ Also, one terminal can send a packet to itself:
|
|||
|
||||
IVy places some restriction on extracts with parameters. These
|
||||
restrictions guarantee that the parallel processes behave as if they
|
||||
were running sequentially in a single procees space (technically, the
|
||||
were running sequentially in a single process space (technically, the
|
||||
Ivy guarantees that the actions are
|
||||
[*serializable*](https://en.wikipedia.org/wiki/Serializability)). We'll
|
||||
discuss these restrictions shortly. For now let's look at using the
|
||||
|
|
@ -197,20 +197,20 @@ discuss these restrictions shortly. For now let's look at using the
|
|||
# Running a distributed protocol
|
||||
|
||||
Recall that the leader election protocol had an interface `trans` that
|
||||
represented the network. Since this interace has the same specification
|
||||
represented the network. Since this interface has the same specification
|
||||
`udp_simple`, we can replace object `trans` with this code:
|
||||
|
||||
include udp
|
||||
instance trans : udp_simple(node.t,id.t)
|
||||
|
||||
Notice, we use `node.t` as the `addr` type and `id.t` as the `pkt`
|
||||
Notice that we use `node.t` as the `addr` type and `id.t` as the `pkt`
|
||||
type. We also have to remove these declarations:
|
||||
|
||||
import trans.send
|
||||
export trans.recv
|
||||
|
||||
This is because `send` is now privided by `trans`, and `recv` is now
|
||||
called by `trans`. The environment is now just:
|
||||
This is because `send` is now provided by `trans`, and `recv` is now
|
||||
called by `trans`, not by the REPL. The environment is now just:
|
||||
|
||||
import serv.elect
|
||||
export app.async
|
||||
|
|
@ -218,10 +218,10 @@ called by `trans`. The environment is now just:
|
|||
Finally, we change the `extract` declaration to include the
|
||||
*implementation* of `trans`:
|
||||
|
||||
extract iso_impl(me) = app(me),trans.impl(me),node_impl,id_impl,asgn
|
||||
extract iso_impl(me:node.t) = app(me),trans.impl(me),node_impl,id_impl,asgn
|
||||
|
||||
That is, we don't want the specification object `trans.spec` in the
|
||||
code we actually run. Notice that we strip the first parameter of bot
|
||||
code we actually run. Notice that we strip the first parameter of both
|
||||
`app` and `trans.impl`. We don't strip parameters from `node_impl`,
|
||||
`id_impl`, `asgn` because these objects provide functions without any
|
||||
state (they are a bit like static methods in a C++ class). We'll
|
||||
|
|
@ -243,10 +243,10 @@ of `trans` hasn't changed, so our inductive invariant is still good.
|
|||
We might ask why we didn't have to verify `trans.impl`. This is
|
||||
because this object is part of IVy's trusted code base. In fact,
|
||||
`udp_simple` is implemented in C++ and makes use of the operating
|
||||
system's API, which we can't formally verify. We can only verify this
|
||||
object by testing.
|
||||
system's API, which we can't formally verify. We can only verify
|
||||
`trans.impl` by testing.
|
||||
|
||||
For now, let's try to run our protol. As before, we compile it like this:
|
||||
For now, let's try to run our protocol. As before, we compile it like this:
|
||||
|
||||
$ ivy_to_cpp target=repl isolate=iso_impl leader_election_ring_udp.ivy
|
||||
$ g++ -o leader_election_ring_udp leader_election_ring_udp.cpp
|
||||
|
|
@ -284,7 +284,7 @@ Clearly, node 1's id did not pass node 0, so node 1 is not elected.
|
|||
Our protocol works, but is still unsatisfactory in at least one
|
||||
way. That is, it only does something in response to a call to
|
||||
`app.async`. We'd like `app.async` to be connected to some kind of
|
||||
system event to it repeasts at some interval. We can do this using the
|
||||
system event so it repeats at some interval. We can do this using the
|
||||
system `timeout` module. This contains the following interface:
|
||||
|
||||
module timeout_sec = {
|
||||
|
|
@ -316,9 +316,9 @@ To test, this interface, let's write a simple program that just imports
|
|||
|
||||
Here's what we get:
|
||||
|
||||
ivy_to_cpp target=repl timeout_test.ivy
|
||||
g++ -o timeout_test timeout_test.cpp
|
||||
./timeout_test
|
||||
$ ivy_to_cpp target=repl timeout_test.ivy
|
||||
$ g++ -o timeout_test timeout_test.cpp
|
||||
$ ./timeout_test
|
||||
> foo.timeout
|
||||
foo.timeout
|
||||
foo.timeout
|
||||
|
|
@ -348,7 +348,7 @@ process. We also have to remove this line, since action `app.async` no longer ex
|
|||
|
||||
Finally, we include the implementation of `sec` in the extract:
|
||||
|
||||
extract iso_impl(me) = app(me),trans.impl(me),sec.impl(me),node_impl,id_impl,asgn
|
||||
extract iso_impl(me:node.t) = app(me),trans.impl(me),sec.impl(me),node_impl,id_impl,asgn
|
||||
|
||||
Notice that `sec.impl` also has one parameter stripped, since we have
|
||||
one timer per process. We compile as before:
|
||||
|
|
@ -358,10 +358,10 @@ one timer per process. We compile as before:
|
|||
|
||||
Now we run the processes in terminals A and B:
|
||||
|
||||
A: $ ./leader_election_ring_udp 0
|
||||
A: $ ./leader_election_ring_udp2 0
|
||||
A: >
|
||||
|
||||
B: $ ./leader_election_ring_udp 1
|
||||
B: $ ./leader_election_ring_udp2 1
|
||||
B: >
|
||||
|
||||
A: serve.elect
|
||||
|
|
@ -369,7 +369,7 @@ Now we run the processes in terminals A and B:
|
|||
A: serve.elect
|
||||
...
|
||||
|
||||
Notice the nothing happens when we start node 0. It is sending packets
|
||||
Notice that nothing happens when we start node 0. It is sending packets
|
||||
once per second, but they are being dropped because no port is yet
|
||||
open to receive them. After we start node 1, it forwards node 0's
|
||||
packets, which causes node 0 to be elected (and to continues to be
|
||||
|
|
@ -386,16 +386,16 @@ deal with this problem when we consider
|
|||
[liveness](https://en.wikipedia.org/wiki/Liveness) specifications.
|
||||
IVy will however, warn us that there might be a problem:
|
||||
|
||||
ivy_to_cpp target=repl isolate=iso_impl leader_election_ring_udp2.ivy
|
||||
$ ivy_to_cpp target=repl isolate=iso_impl leader_election_ring_udp2.ivy
|
||||
leader_election_ring_udp2.ivy: line 131: warning: action sec.timeout is never called
|
||||
|
||||
## Serializability
|
||||
|
||||
As mentioned above, IVy guarantees serializability. This means that
|
||||
actions executed by concurrent process produce the same input/output
|
||||
result as if the actions had been executed *in isolation* in some
|
||||
order. By isolation, we mean that each action completes before the next
|
||||
action begins.
|
||||
result as if the actions had been executed [*in isolation*](https://en.wikipedia.org/wiki/ACID) in some
|
||||
order. By isolation, we mean that each action completes before any other action
|
||||
begins.
|
||||
|
||||
To guarantee serializability, IVy requires that processes be
|
||||
*non-interfering*. This means that one process cannot have a
|
||||
|
|
@ -417,11 +417,11 @@ As an example of interference, consider the following program:
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
This program has one parallel process for each value of a type
|
||||
`t`. Each process provides a method that modifies a global variable
|
||||
`bit`. Obviously, this is not a distributed program, becuase the processes
|
||||
`bit`. Obviously, this is not a distributed program, because the processes
|
||||
share a variable. Here's what happens when we try to compile the program:
|
||||
|
||||
ivy_to_cpp target=repl isolate=iso_foo interference2.ivy
|
||||
|
|
@ -449,7 +449,7 @@ process:
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me),bit(me)
|
||||
extract iso_foo(me:t) = foo(me),bit(me)
|
||||
|
||||
This program compiles successfully. But what would happen if
|
||||
one process tried to access the variable of another process.
|
||||
|
|
@ -469,7 +469,7 @@ Consider this program:
|
|||
|
||||
export foo.flip
|
||||
|
||||
extract iso_foo(me) = foo(me),bit(me)
|
||||
extract iso_foo(me:t) = foo(me),bit(me)
|
||||
|
||||
Here, object `foo(me)` accesses the `bit` of some process `x`,
|
||||
where `x` is an input. Here's what happens when we compile:
|
||||
|
|
@ -487,13 +487,13 @@ Of course, to communicate with each other, processes must have a
|
|||
visible effect on something. That something is the environment, which
|
||||
includes the operating system and the physical network. A call to
|
||||
`trans.send` has an an effect on the environment, namely sending a
|
||||
packet. The Ivy runtime guarantees, however, that actions remain
|
||||
packet. The Ivy run-time guarantees, however, that actions remain
|
||||
serializable despite these effects, using [Lipton's theory of left-movers
|
||||
and right-movers](http://dl.acm.org/citation.cfm?id=361234). In the theory's terms,
|
||||
receiving a packet is right-mover, while sending a packet is a
|
||||
left-mover. Every action consists of zero or one receive events followed by
|
||||
any number of send events. The theory tells use that such actions are
|
||||
serializable. That is, we can re-orer any concurrent execution by
|
||||
serializable. That is, we can re-order any concurrent execution by
|
||||
commuting left-movers and right-movers such that the result is an
|
||||
equivalent isolated execution.
|
||||
|
||||
|
|
@ -508,29 +508,29 @@ Ivy allows immutable objects (that is, read-only objects) such as the
|
|||
`pid` map in the leader protocol, to be shared between processes.
|
||||
Each process refers to its own local copy of the immutable object. In
|
||||
the case of the `pid` map, IVy solved for a value of this function
|
||||
satisfying the given axiom that no to nodes have the same id. A table
|
||||
satisfying the given axiom that no two nodes have the same id. A table
|
||||
of this function was stored in the compiled process.
|
||||
|
||||
Currently, IVy has some limitations in its ability to generate the
|
||||
immutable objects and also to generate initial states for paramterized
|
||||
immutable objects and also to generate initial states for parametrized
|
||||
processes. Consider, for example, this program:
|
||||
|
||||
#lang ivy1.6
|
||||
#lang ivy1.6
|
||||
|
||||
type t
|
||||
|
||||
object foo(me:t) = {
|
||||
individual bit:bool
|
||||
init ~bit
|
||||
individual bit:bool
|
||||
init ~bit
|
||||
|
||||
action get_bit returns (x:bool) = {
|
||||
x := bit
|
||||
}
|
||||
action get_bit returns (x:bool) = {
|
||||
x := bit
|
||||
}
|
||||
}
|
||||
|
||||
export foo.get_bit
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
IVy can compile this program and run it:
|
||||
|
||||
|
|
@ -543,16 +543,50 @@ But suppose we change the initial condition so it depends on the stripped parame
|
|||
|
||||
init bit <-> me = 0
|
||||
|
||||
That is, we want `bit` to be true initially only for process 0. Here's what happens when we try to comppile:
|
||||
That is, we want `bit` to be true initially only for process 0. Here's what happens when we try to compile:
|
||||
|
||||
ivy_to_cpp target=repl isolate=iso_foo paraminit2.ivy
|
||||
paraminit2.ivy: line 7: error: initial condition depends on stripped parameter
|
||||
|
||||
IVy isn't smart enough to compile an initial condition that is a
|
||||
function of the stripped parameter.
|
||||
function of the stripped parameter. We can work around this by
|
||||
providing this function explicitly, using an initializer:
|
||||
|
||||
#lang ivy1.6
|
||||
|
||||
type t
|
||||
|
||||
object foo(me:t) = {
|
||||
function bit:bool
|
||||
|
||||
after init {
|
||||
bit := (me = 0)
|
||||
}
|
||||
|
||||
action get_bit returns (x:bool) = {
|
||||
x := bit
|
||||
}
|
||||
}
|
||||
|
||||
export foo.get_bit
|
||||
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
This version can be stripped and gives the expected result:
|
||||
|
||||
$ ivy_to_cpp target=repl isolate=iso_foo paraminit3.ivy
|
||||
$ g++ -o paraminit3 paraminit3.cpp
|
||||
$ ./paraminit3 0
|
||||
> foo.get_bit
|
||||
1
|
||||
> ^C
|
||||
$ ./paraminit3 1
|
||||
> foo.get_bit
|
||||
0
|
||||
>
|
||||
|
||||
|
||||
|
||||
# Aspects
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -13,5 +13,5 @@ object foo(me:t) = {
|
|||
|
||||
export foo.get_bit
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
|
|
|
|||
|
|
@ -13,5 +13,5 @@ object foo(me:t) = {
|
|||
|
||||
export foo.get_bit
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
|
|
|
|||
|
|
@ -2,19 +2,19 @@
|
|||
|
||||
type t
|
||||
|
||||
object foo = {
|
||||
function bit(X:t):bool
|
||||
object foo(me:t) = {
|
||||
function bit:bool
|
||||
|
||||
after init {
|
||||
bit(X) := (X = 0)
|
||||
bit := (me = 0)
|
||||
}
|
||||
|
||||
action get_bit (me:t) returns (x:bool) = {
|
||||
x := bit(me)
|
||||
action get_bit returns (x:bool) = {
|
||||
x := bit
|
||||
}
|
||||
}
|
||||
|
||||
export foo.get_bit
|
||||
|
||||
extract iso_foo(me) = foo(me)
|
||||
extract iso_foo(me:t) = foo(me)
|
||||
|
||||
|
|
|
|||
|
|
@ -12,4 +12,4 @@ export foo.send
|
|||
interpret a->bv[1]
|
||||
interpret p->bv[16]
|
||||
|
||||
extract iso_impl(me) = foo.impl(me)
|
||||
extract iso_impl(me:a) = foo.impl(me)
|
||||
|
|
|
|||
|
|
@ -692,6 +692,20 @@ For example:
|
|||
|
||||
In this case, calling `c(id).my_id` will return `id`.
|
||||
|
||||
An alternative way to write the above would be:
|
||||
|
||||
type id_t
|
||||
|
||||
object c(id:id_t) = {
|
||||
action my_id returns (x:id_t) = {
|
||||
x := id
|
||||
}
|
||||
}
|
||||
|
||||
Notice that the object parameter is given as a logical constant rather
|
||||
than a variable. This constant can be referred to in the body of the
|
||||
object.
|
||||
|
||||
## Monitors
|
||||
|
||||
While embedding assertions in code is a useful way to write
|
||||
|
|
@ -955,6 +969,81 @@ Roughly speaking, this means that assertions about an object's inputs
|
|||
are assumptions for that object, while assertions about its outputs
|
||||
are guarantees.
|
||||
|
||||
## Initializers
|
||||
|
||||
In some cases it is awkward to give the initial condition as a
|
||||
formula. An alternative is to use an initializer. This is a special
|
||||
action that is executed once initially, before any exported actions
|
||||
are called. For example:
|
||||
|
||||
individual bit : bool
|
||||
|
||||
after init {
|
||||
bit := false
|
||||
}
|
||||
|
||||
This behaves like a monitor after a special internal action called
|
||||
`init`. As the `after` implies, the initial condition prescribed by
|
||||
the `init` declarations is assumed to be established before any
|
||||
initializers are called. Initializers are executed in the order they
|
||||
are declared.
|
||||
|
||||
Initializers may call other actions. For example, suppose we have a
|
||||
module `collection` representing a set of objects that is initially
|
||||
empty. If we wanted a set that initially contained the value zero, we
|
||||
could use an initializer like this:
|
||||
|
||||
type t
|
||||
|
||||
object foo = {
|
||||
instance myset : collection(t)
|
||||
|
||||
after init {
|
||||
call myset.add(0)
|
||||
}
|
||||
}
|
||||
|
||||
This action is called exactly once after `myset` is initialized.
|
||||
|
||||
Parameterized objects can also have initializers. For example, we may
|
||||
want to have a collection of objects that each contain a bit, where initially
|
||||
only the bit of object 0 is true:
|
||||
|
||||
type t
|
||||
|
||||
object foo(self:t) = {
|
||||
individual bit : bool
|
||||
|
||||
after init {
|
||||
bit := (self = 0)
|
||||
}
|
||||
}
|
||||
|
||||
There are some restrictions in initializers of parameterized objects,
|
||||
however. These are:
|
||||
|
||||
- Conditions of `if` statements may not refer to the parameter, and
|
||||
|
||||
- In assignments, the left-hand side must contain the parameter if the right-hand side does.
|
||||
|
||||
For example, this initializer would not be legal:
|
||||
|
||||
type t
|
||||
|
||||
individual bit : bool
|
||||
|
||||
object foo(self:t) = {
|
||||
after init {
|
||||
bit := (self = 0)
|
||||
}
|
||||
}
|
||||
|
||||
This is because the component `bit` being assigned is not
|
||||
parameterized. This means it is in effect being assigned a different
|
||||
value for each value of `self`. The restrictions guarantee that the
|
||||
result of the initializer does not depend on the order in which it is
|
||||
called for different parameter values.
|
||||
|
||||
## Interpreted types and theories
|
||||
|
||||
The normal way of using IVy is to declare uninterpreted types and to
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ from ivy_logic_utils import to_clauses, formula_to_clauses, substitute_constants
|
|||
substitute_clause, substitute_ast, used_symbols_clauses, used_symbols_ast, rename_clauses, subst_both_clauses,\
|
||||
variables_distinct_ast, is_individual_ast, variables_distinct_list_ast, sym_placeholders, sym_inst, apps_ast,\
|
||||
eq_atom, eq_lit, eqs_ast, TseitinContext, formula_to_clauses_tseitin,\
|
||||
used_symbols_asts, symbols_asts, has_enumerated_sort, false_clauses, true_clauses, or_clauses, dual_formula, Clauses, and_clauses, substitute_constants_ast, rename_ast, bool_const
|
||||
used_symbols_asts, symbols_asts, has_enumerated_sort, false_clauses, true_clauses, or_clauses, dual_formula, Clauses, and_clauses, substitute_constants_ast, rename_ast, bool_const, used_variables_ast
|
||||
from ivy_transrel import state_to_action,new, compose_updates, condition_update_on_fmla, hide, join_action,\
|
||||
subst_action, null_update, exist_quant, hide_state, hide_state_map, constrain_state
|
||||
from ivy_utils import unzip_append, IvyError, IvyUndefined, distinct_obj_renaming, dbg
|
||||
|
|
@ -319,6 +319,10 @@ class AssignAction(Action):
|
|||
else:
|
||||
rhs = add_parameters_ast(rhs,extend)
|
||||
|
||||
lhs_vars = used_variables_ast(lhs)
|
||||
if any(v not in lhs_vars for v in used_variables_ast(rhs)):
|
||||
raise IvyError(self,"multiply assigned: {}".format(lhs.rep))
|
||||
|
||||
type_check(domain,rhs)
|
||||
if is_individual_ast(lhs) != is_individual_ast(rhs):
|
||||
# print type(lhs.rep)
|
||||
|
|
@ -884,3 +888,7 @@ def action_def_to_str(name,action):
|
|||
else:
|
||||
res += '{' + str(action) + '}'
|
||||
return res
|
||||
|
||||
def has_code(action):
|
||||
return any(not isinstance(a,Sequence) for a in action.iter_subactions())
|
||||
|
||||
|
|
|
|||
|
|
@ -12,6 +12,7 @@ from string import *
|
|||
import copy
|
||||
import functools
|
||||
import pickle
|
||||
import ivy_actions
|
||||
|
||||
|
||||
################################################################################
|
||||
|
|
@ -104,8 +105,17 @@ class AnalysisGraph(object):
|
|||
if ic == None:
|
||||
ic = im.init_cond
|
||||
s = self.domain.new_state(ic)
|
||||
s2 = self.domain.new_state(ic)
|
||||
self.add(s2,s)
|
||||
if self.domain.initializers:
|
||||
action = ivy_actions.Sequence(*[a for n,a in self.domain.initializers])
|
||||
s = action_app(action,s)
|
||||
with AC(self,no_add=True):
|
||||
with EvalContext(check=False):
|
||||
s2 = eval_state(s)
|
||||
s2.expr = s
|
||||
self.add(s2)
|
||||
else:
|
||||
s2 = self.domain.new_state(ic)
|
||||
self.add(s2,s)
|
||||
if abstractor:
|
||||
abstractor(s2)
|
||||
# print "initial state: {}".format(s2)
|
||||
|
|
|
|||
|
|
@ -23,10 +23,10 @@ coverage = iu.BooleanParameter("coverage",True)
|
|||
|
||||
|
||||
def display_cex(msg,ag):
|
||||
print msg
|
||||
if diagnose.get():
|
||||
ui.ui_main_loop(ag)
|
||||
exit(1)
|
||||
exit(1)
|
||||
raise iu.IvyError(None,msg)
|
||||
|
||||
def check_properties():
|
||||
if itp.false_properties():
|
||||
|
|
@ -87,6 +87,10 @@ def check_module():
|
|||
ivy_isolate.create_isolate(isolate) # ,ext='ext'
|
||||
check_properties()
|
||||
ag = ivy_art.AnalysisGraph(initializer=ivy_alpha.alpha)
|
||||
if im.module.initializers:
|
||||
cex = ag.check_bounded_safety(ag.states[0])
|
||||
if cex is not None:
|
||||
display_cex("safety failed in initializer",cex)
|
||||
with ivy_interp.EvalContext(check=False):
|
||||
check_conjectures('Initiation','These conjectures are false initially.',ag,ag.states[0])
|
||||
for a in sorted(im.module.public_actions):
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ from ivy_interp import Interp, eval_state_facts
|
|||
from functools import partial
|
||||
from ivy_concept_space import *
|
||||
from ivy_parser import parse,ConstantDecl,ActionDef
|
||||
from ivy_actions import DerivedUpdate, type_check_action, type_check, SymbolList, UpdatePattern, ActionContext, LocalAction, AssignAction, CallAction, Sequence, IfAction, AssertAction, AssumeAction, NativeAction
|
||||
from ivy_actions import DerivedUpdate, type_check_action, type_check, SymbolList, UpdatePattern, ActionContext, LocalAction, AssignAction, CallAction, Sequence, IfAction, AssertAction, AssumeAction, NativeAction, has_code
|
||||
from ivy_utils import IvyError
|
||||
import ivy_logic
|
||||
import ivy_dafny_compiler as dc
|
||||
|
|
@ -21,6 +21,7 @@ import ivy_alpha
|
|||
import ivy_module as im
|
||||
import ivy_theory as ith
|
||||
import ivy_isolate as iso
|
||||
import ivy_printer
|
||||
from collections import defaultdict
|
||||
|
||||
class IvyDeclInterp(object):
|
||||
|
|
@ -552,6 +553,7 @@ def check_instantiations(mod,decls):
|
|||
raise IvyError(inst,"{} undefined in instantiation".format(inst.relname))
|
||||
|
||||
|
||||
|
||||
def ivy_compile(decls,mod=None,create_isolate=True,**kwargs):
|
||||
mod = mod or im.module
|
||||
with mod.sig:
|
||||
|
|
@ -584,7 +586,6 @@ def ivy_compile(decls,mod=None,create_isolate=True,**kwargs):
|
|||
iso.create_isolate(isolate.get(),mod,**kwargs)
|
||||
|
||||
|
||||
|
||||
def clear_rules(modname):
|
||||
import sys
|
||||
if modname in sys.modules:
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ import ivy_theory as ith
|
|||
import ivy_concept_space as ics
|
||||
from ivy_ast import ASTContext
|
||||
from collections import defaultdict
|
||||
import ivy_printer
|
||||
|
||||
show_compiled = iu.BooleanParameter("show_compiled",False)
|
||||
cone_of_influence = iu.BooleanParameter("coi",True)
|
||||
|
|
@ -149,19 +150,27 @@ def set_interpret_all_sorts(t):
|
|||
#def startswith_some(s,prefixes):
|
||||
# return any(s.startswith(name+iu.ivy_compose_character) for name in prefixes)
|
||||
|
||||
def startswith_some(s,prefixes,mod):
|
||||
def startswith_some_rec(s,prefixes,mod):
|
||||
if s in mod.privates:
|
||||
return False
|
||||
parts = s.rsplit(iu.ivy_compose_character,1)
|
||||
return len(parts)==2 and startswith_eq_some(parts[0],prefixes,mod)
|
||||
return len(parts)==2 and startswith_eq_some_rec(parts[0],prefixes,mod)
|
||||
|
||||
#def startswith_eq_some(s,prefixes):
|
||||
# return any(s.startswith(name+iu.ivy_compose_character) or s == name for name in prefixes)
|
||||
|
||||
def startswith_eq_some(s,prefixes,mod):
|
||||
def startswith_eq_some_rec(s,prefixes,mod):
|
||||
if s in prefixes:
|
||||
return True
|
||||
return startswith_some(s,prefixes,mod)
|
||||
return startswith_some_rec(s,prefixes,mod)
|
||||
|
||||
def startswith_some(s,prefixes,mod):
|
||||
s = implementation_map.get(s,s)
|
||||
return startswith_some_rec(s,prefixes,mod)
|
||||
|
||||
def startswith_eq_some(s,prefixes,mod):
|
||||
s = implementation_map.get(s,s)
|
||||
return startswith_eq_some_rec(s,prefixes,mod)
|
||||
|
||||
def strip_map_lookup(name,strip_map,with_dot=False):
|
||||
name = canon_act(name)
|
||||
|
|
@ -197,7 +206,8 @@ def strip_action(ast,strip_map,strip_binding):
|
|||
return ast.clone([call]+[strip_action(arg,strip_map,strip_binding) for arg in ast.args[1:]])
|
||||
if isinstance(ast,ia.AssignAction):
|
||||
if ast.args[0].rep.name in ivy_logic.sig.symbols:
|
||||
if len(strip_map_lookup(ast.args[0].rep.name,strip_map)) != num_isolate_params:
|
||||
lhs_params = strip_map_lookup(ast.args[0].rep.name,strip_map)
|
||||
if len(lhs_params) != num_isolate_params:
|
||||
raise iu.IvyError(ast,"assignment may be interfering")
|
||||
if (ivy_logic.is_constant(ast) or ivy_logic.is_variable(ast)) and ast in strip_binding:
|
||||
sname = strip_binding[ast]
|
||||
|
|
@ -271,6 +281,11 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip):
|
|||
global strip_added_symbols
|
||||
global num_isolate_params
|
||||
num_isolate_params = len(isolate.params())
|
||||
ips = set(p.rep for p in isolate.params())
|
||||
for atom in isolate.verified()+isolate.present():
|
||||
for p in atom.args:
|
||||
if p.rep not in ips:
|
||||
raise iu.IvyError(p,'unbound isolate parameter: {}'.format(p))
|
||||
strip_added_symbols = []
|
||||
strip_map = {}
|
||||
for atom in isolate.verified() + isolate.present():
|
||||
|
|
@ -294,8 +309,6 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip):
|
|||
new_actions = {}
|
||||
for name,action in mod.actions.iteritems():
|
||||
strip_params = strip_map_lookup(canon_act(name),strip_map,with_dot=False)
|
||||
iu.dbg('strip_params')
|
||||
iu.dbg('action.formal_params')
|
||||
if not(len(action.formal_params) >= len(strip_params)):
|
||||
raise iu.IvyError(action,"cannot strip isolate parameters from {}".format(name))
|
||||
strip_binding = dict(zip(action.formal_params,strip_params))
|
||||
|
|
@ -503,6 +516,8 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None):
|
|||
|
||||
impl_mixins = defaultdict(list)
|
||||
# delegate all the stub actions to their implementations
|
||||
global implementation_map
|
||||
implementation_map = {}
|
||||
for actname,ms in mod.mixins.iteritems():
|
||||
implements = [m for m in ms if isinstance(m,ivy_ast.MixinImplementDef)]
|
||||
impl_mixins[actname].extend(implements)
|
||||
|
|
@ -518,10 +533,7 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None):
|
|||
raise IvyError(m,'multiple implementations of action {}'.format(m.mixee()))
|
||||
action = ia.apply_mixin(m,mod.actions[m.mixer()],action)
|
||||
mod.actions[m.mixee()] = action
|
||||
if startswith_eq_some(m.mixer(),verified,mod):
|
||||
verified.add(m.mixee())
|
||||
if startswith_eq_some(m.mixer(),present,mod):
|
||||
present.add(m.mixee())
|
||||
implementation_map[m.mixee()] = m.mixer()
|
||||
|
||||
new_actions = {}
|
||||
use_mixin = lambda name: startswith_some(name,present,mod)
|
||||
|
|
@ -755,15 +767,6 @@ def hide_action_params(action):
|
|||
res = ia.LocalAction(*(params + [action]))
|
||||
return res
|
||||
|
||||
def labeled_fmlas_to_str(kwd,lfmlas):
|
||||
res = ''
|
||||
for f in lfmlas:
|
||||
res += kwd + ' '
|
||||
if f.label:
|
||||
res += '[{}] '.format(f.label)
|
||||
res += str(f.formula) + '\n'
|
||||
return res
|
||||
|
||||
def get_cone(mod,action_name,cone):
|
||||
if action_name not in cone:
|
||||
cone.add(action_name)
|
||||
|
|
@ -780,20 +783,39 @@ def get_mod_cone(mod):
|
|||
get_cone(mod,a.rep,cone)
|
||||
return cone
|
||||
|
||||
def has_code(action):
|
||||
return any(not isinstance(a,ia.Sequence) for a in action.iter_subactions())
|
||||
def loop_action(action,mod):
|
||||
subst = dict((p,ivy_logic.Variable('Y'+p.name,p.sort)) for p in action.formal_params)
|
||||
action = lu.substitute_constants_ast(action,subst)
|
||||
ia.type_check_action(action,mod) # make sure all is legal
|
||||
return action
|
||||
|
||||
def fix_initializers(mod,after_inits):
|
||||
for m in after_inits:
|
||||
name = m.mixer()
|
||||
extname = 'ext:'+name
|
||||
action = mod.actions[extname] if extname in mod.actions else mod.actions[name]
|
||||
if not ia.has_code(action):
|
||||
continue
|
||||
mod.initializers.append((name,loop_action(action,mod)))
|
||||
if name in mod.actions:
|
||||
del mod.actions[name]
|
||||
if name in mod.public_actions:
|
||||
mod.public_actions.remove(name)
|
||||
if extname in mod.actions:
|
||||
del mod.actions[extname]
|
||||
if extname in mod.public_actions:
|
||||
mod.public_actions.remove(extname)
|
||||
ais = set(m.mixer() for m in after_inits)
|
||||
mod.exports = [e for e in mod.exports if e.exported() not in ais]
|
||||
|
||||
def create_isolate(iso,mod = None,**kwargs):
|
||||
|
||||
mod = mod or im.module
|
||||
|
||||
# make an imaginary init operation:
|
||||
|
||||
init_action = ia.Sequence()
|
||||
init_action.formal_params = []
|
||||
init_action.formal_returns = []
|
||||
init_action.lineno = None
|
||||
mod.actions["init"] = init_action
|
||||
# treat initializers as exports
|
||||
after_inits = mod.mixins["init"]
|
||||
del mod.mixins["init"]
|
||||
mod.exports.extend(ivy_ast.ExportDef(ivy_ast.Atom(a.mixer()),ivy_ast.Atom('')) for a in after_inits)
|
||||
|
||||
# check all mixin declarations
|
||||
|
||||
|
|
@ -879,11 +901,6 @@ def create_isolate(iso,mod = None,**kwargs):
|
|||
for a in mod.actions:
|
||||
mod.public_actions.add(a)
|
||||
|
||||
mod.init_action = mod.actions.get('ext:.init',mod.actions['.init'])
|
||||
del mod.actions['init']
|
||||
del mod.actions['ext:.init']
|
||||
iu.dbg('mod.init_action')
|
||||
|
||||
# Create one big external action if requested
|
||||
|
||||
|
||||
|
|
@ -925,24 +942,17 @@ def create_isolate(iso,mod = None,**kwargs):
|
|||
if a not in cone and not a.startswith('ext:') and a not in mixers:
|
||||
ea = 'ext:' + a
|
||||
if ea in mod.actions and ea not in cone:
|
||||
if has_code(mod.actions[a]):
|
||||
if ia.has_code(mod.actions[a]):
|
||||
iu.warn(mod.actions[a],"action {} is never called".format(a))
|
||||
|
||||
fix_initializers(mod,after_inits)
|
||||
|
||||
# show the compiled code if requested
|
||||
|
||||
if show_compiled.get():
|
||||
print ivy_logic.sig
|
||||
thing = ''
|
||||
for kwd,lst in [('axiom',mod.labeled_axioms),
|
||||
('property',mod.labeled_props),
|
||||
('init',mod.labeled_inits),
|
||||
('conjecture',mod.labeled_conjs),]:
|
||||
thing += labeled_fmlas_to_str(kwd,lst)
|
||||
for tn in sorted(mod.sig.interp):
|
||||
thing += "interp {} -> {}\n".format(tn,mod.sig.interp[tn])
|
||||
print thing
|
||||
for x,y in mod.actions.iteritems():
|
||||
print iu.pretty(ia.action_def_to_str(x,y))
|
||||
ivy_printer.print_module(mod)
|
||||
|
||||
|
||||
|
||||
def has_assertions(mod,callee):
|
||||
return any(isinstance(action,ia.AssertAction) for action in mod.actions[callee].iter_subactions())
|
||||
|
|
@ -966,6 +976,8 @@ def check_isolate_completeness(mod = None):
|
|||
checked_context = defaultdict(set) # maps action name to set of delegees
|
||||
delegates = set(s.delegated() for s in mod.delegates if not s.delegee())
|
||||
delegated_to = dict((s.delegated(),s.delegee()) for s in mod.delegates if s.delegee())
|
||||
global implementation_map
|
||||
implementation_map = {}
|
||||
for iso_name,isolate in mod.isolates.iteritems():
|
||||
verified = set(a.relname for a in isolate.verified())
|
||||
present = set(a.relname for a in isolate.present())
|
||||
|
|
|
|||
|
|
@ -56,6 +56,7 @@ class Module(object):
|
|||
self.privates = set() # set of string (names of private actions)
|
||||
self.interps = defaultdict(list) # maps type names to lists of labeled interpretions
|
||||
self.natives = [] # list of NativeDef
|
||||
self.initializers = [] # list of name,action pairs
|
||||
self.params = []
|
||||
|
||||
self.sig = il.sig.copy() # capture the current signature
|
||||
|
|
|
|||
|
|
@ -711,23 +711,23 @@ if not (iu.get_numeric_version() <= [1,1]):
|
|||
atom.lineno = get_lineno(p,3)
|
||||
handle_before_after("implement",atom,p[7],p[0],p[4],p[5])
|
||||
def p_top_isolate_callatom_eq_callatoms(p):
|
||||
'top : top ISOLATE callatom EQ callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([p[3]] + p[5])))
|
||||
'top : top ISOLATE SYMBOL optargs EQ callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([Atom(p[3],p[4])] + p[6])))
|
||||
d.args[0].with_args = 0
|
||||
d.lineno = get_lineno(p,2)
|
||||
p[0] = p[1]
|
||||
p[0].declare(d)
|
||||
def p_top_isolate_callatom_eq_callatoms_with_callatoms(p):
|
||||
'top : top ISOLATE callatom EQ callatoms WITH callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([p[3]] + p[5] + p[7])))
|
||||
d.args[0].with_args = len(p[7])
|
||||
'top : top ISOLATE SYMBOL optargs EQ callatoms WITH callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([Atom(p[3],p[4])] + p[6] + p[8])))
|
||||
d.args[0].with_args = len(p[8])
|
||||
d.lineno = get_lineno(p,2)
|
||||
p[0] = p[1]
|
||||
p[0].declare(d)
|
||||
def p_top_extract_callatom_eq_callatoms(p):
|
||||
'top : top EXTRACT callatom EQ callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([p[3]] + p[5])))
|
||||
d.args[0].with_args = len(p[5])
|
||||
'top : top EXTRACT SYMBOL optargs EQ callatoms'
|
||||
d = IsolateDecl(IsolateDef(*([Atom(p[3],p[4])] + p[6])))
|
||||
d.args[0].with_args = len(p[6])
|
||||
d.lineno = get_lineno(p,2)
|
||||
p[0] = p[1]
|
||||
p[0].declare(d)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,30 @@
|
|||
import ivy_logic
|
||||
import ivy_utils as iu
|
||||
import ivy_actions as ia
|
||||
|
||||
def labeled_fmlas_to_str(kwd,lfmlas):
|
||||
res = ''
|
||||
for f in lfmlas:
|
||||
res += kwd + ' '
|
||||
if f.label:
|
||||
res += '[{}] '.format(f.label)
|
||||
res += str(f.formula) + '\n'
|
||||
return res
|
||||
|
||||
def print_module(mod):
|
||||
print ivy_logic.sig
|
||||
thing = ''
|
||||
for kwd,lst in [('axiom',mod.labeled_axioms),
|
||||
('property',mod.labeled_props),
|
||||
('init',mod.labeled_inits),
|
||||
('conjecture',mod.labeled_conjs),]:
|
||||
thing += labeled_fmlas_to_str(kwd,lst)
|
||||
for tn in sorted(mod.sig.interp):
|
||||
thing += "interp {} -> {}\n".format(tn,mod.sig.interp[tn])
|
||||
print thing
|
||||
|
||||
for name,action in mod.initializers:
|
||||
print iu.pretty("after init {" + str(action) + "}")
|
||||
|
||||
for x,y in mod.actions.iteritems():
|
||||
print iu.pretty(ia.action_def_to_str(x,y))
|
||||
|
|
@ -890,6 +890,9 @@ def emit_one_initial_state(header):
|
|||
header.append(' this->{} = {};\n'.format(name,name))
|
||||
elif sym not in is_derived:
|
||||
assign_symbol_from_model(header,sym,m)
|
||||
action = ia.Sequence(*[a for n,a in im.module.initializers])
|
||||
action.emit(header)
|
||||
|
||||
|
||||
|
||||
def emit_constant(self,header,code):
|
||||
|
|
|
|||
|
|
@ -0,0 +1,47 @@
|
|||
|
||||
from ivy import ivy_module as im
|
||||
from ivy.ivy_compiler import ivy_from_string
|
||||
from ivy.tk_ui import new_ui
|
||||
from ivy import ivy_utils as iu
|
||||
|
||||
prog = """#lang ivy1.6
|
||||
|
||||
type t
|
||||
|
||||
individual x(X:t) : t
|
||||
|
||||
object foo(me:t) = {
|
||||
after init {
|
||||
x(me) := me;
|
||||
assert false
|
||||
}
|
||||
}
|
||||
|
||||
isolate iso_foo(me:t) = foo(me) with x(me)
|
||||
|
||||
"""
|
||||
|
||||
with im.Module():
|
||||
iu.set_parameters({'mode':'induction','isolate':'iso_foo','show_compiled':'true'})
|
||||
main_ui = new_ui()
|
||||
ui = main_ui.add(ivy_from_string(prog))
|
||||
main_ui.tk.update_idletasks()
|
||||
main_ui.answer("OK")
|
||||
ui.check_safety_node(ui.node(0))
|
||||
assert not ui.node(0).safe
|
||||
# ui.check_inductiveness()
|
||||
# # ui = ui.cti
|
||||
# cg = ui.current_concept_graph
|
||||
# cg.show_relation(cg.relation('link(X,Y)'),'+')
|
||||
# cg.gather()
|
||||
# main_ui.answer("OK")
|
||||
# cg.strengthen()
|
||||
# main_ui.answer("OK")
|
||||
# ui.check_inductiveness()
|
||||
# # cg.show_relation(cg.relation('semaphore'),'+')
|
||||
# cg.gather()
|
||||
# main_ui.answer("View")
|
||||
# cg.bmc_conjecture(bound=1)
|
||||
# main_ui.mainloop()
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
|
||||
from ivy import ivy_module as im
|
||||
from ivy.ivy_compiler import ivy_from_string
|
||||
from ivy.tk_ui import new_ui
|
||||
from ivy import ivy_utils as iu
|
||||
from ivy import ivy_check as ick
|
||||
from ivy import ivy_utils as iu
|
||||
|
||||
prog = """#lang ivy1.6
|
||||
|
||||
type t
|
||||
|
||||
individual x(X:t) : t
|
||||
|
||||
object foo(me:t) = {
|
||||
after init {
|
||||
x(me) := me;
|
||||
assert false
|
||||
}
|
||||
}
|
||||
|
||||
isolate iso_foo(me:t) = foo(me) with x(me)
|
||||
|
||||
"""
|
||||
|
||||
with im.Module():
|
||||
iu.set_parameters({'mode':'induction','isolate':'iso_foo','show_compiled':'true'})
|
||||
ivy_from_string(prog,create_isolate=False)
|
||||
try:
|
||||
ick.check_module()
|
||||
assert False,"safety should have failed"
|
||||
except iu.IvyError as e:
|
||||
print e
|
||||
assert str(e) == "error: safety failed in initializer"
|
||||
|
|
@ -28,7 +28,7 @@ module mod(me) = {
|
|||
|
||||
instance inst(X:foo) : mod(X)
|
||||
|
||||
isolate iso = inst(me)
|
||||
isolate iso(me:foo) = inst(me)
|
||||
|
||||
export inst.set_me
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ module mod(me) = {
|
|||
|
||||
instance inst(X:foo) : mod(X)
|
||||
|
||||
isolate iso = inst(me) with inst(me).baz
|
||||
isolate iso(me:foo) = inst(me) with inst(me).baz
|
||||
|
||||
export inst.set_me
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ instance inst(X:foo) : mod(X)
|
|||
|
||||
axiom inst(X).r & inst(X).x = X
|
||||
|
||||
isolate iso = inst(me)
|
||||
isolate iso(me:foo) = inst(me)
|
||||
|
||||
export inst.set_me
|
||||
"""
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче