Modeling Constraints and Assertions
E
x
e
r
c
i
s
e
1
–
C
o
u
n
t
e
r
M
o
d
e
l
Define
the
init
function
and
set
n
as
0.
Increment
counter
other than last
Always
greater
than
or
equal
to
zero.
Counter’s
value
never
decreases.
E
x
e
r
c
i
s
e
2
–
I
m
a
g
e
F
i
l
e
(
e
a
g
e
r
i
n
i
t
i
a
l
i
z
a
t
i
o
n
)
Except
File/ImageFile
already
stored
in
the
state
E
x
e
r
c
i
s
e
2
–
I
m
a
g
e
F
i
l
e
(
e
a
g
e
r
i
n
i
t
i
a
l
i
z
a
t
i
o
n
)
Always
return
non-
null.
Always
return
the
same
value,
for
a
particular
image.
Inv1
:
getImage
always
return
non-null.
Inv2
:
getImage
always
returns
the
same
value.
E
x
e
r
c
i
s
e
2
–
I
m
a
g
e
F
i
l
e
(
l
a
z
y
i
n
i
t
i
a
l
i
z
a
t
i
o
n
)
Lazy
initialization
Two
cases
to
proceed
the
state
from
s
->
s’
Check
if
already
loaded
E
x
e
r
c
i
s
e
2
–
I
m
a
g
e
F
i
l
e
(
l
a
z
y
i
n
i
t
i
a
l
i
z
a
t
i
o
n
)
Shouldn’t
be
null.
Always
return
the
same
value,
for
a
particular
image.
Inv1
:
getImage
always
return
non-null.
Inv2
:
getImage
always
returns
the
same
value.
E
x
e
r
c
i
s
e
3
–
A
s
s
e
r
t
i
o
n
a
n
d
C
o
u
n
t
e
r
e
x
a
m
p
l
e
s
X
0,0
is
a
Boolean
variable.
Define
constraint
and
assertions
for
only
one
node.
Given
constraint,
can
we
violate
the
assertion?
•
Every
node
must
point
to
one
and
only
one
node.
•
Then
whether
for
every
node,
it
is
pointed
by
one
and
only
one
node?
Solving Boolean constraints are usually super efficient.
E
x
e
r
c
i
s
e
3
–
A
s
s
e
r
t
i
o
n
a
n
d
C
o
u
n
t
e
r
e
x
a
m
p
l
e
s
Definition
constraint
and
assertions
for
two
nodes.
All
the
possibilities.
Assertion.
Counter
example!
E
x
e
r
c
i
s
e
3
–
A
d
d
a
“
p
r
e
v
”
e
d
g
e
Enhancement:
A
new
fact:
Every
node
is
pointed
by
no
more
than
one
node.
E
x
e
r
c
i
s
e
3
–
A
d
d
a
“
p
r
e
v
”
e
d
g
e
Define
constraint
and
assertions
for
only
one
node.
Constraint.
Assertion.
Given
constraint,
can
we
violate
the
assertion?
E
x
e
r
c
i
s
e
3
–
A
d
d
a
“
p
r
e
v
”
e
d
g
e
Definition
constraint
and
assertions
for
two
nodes.
Constraint.
Assertion.
Given
constraint,
can
we
violate
the
assertion?
E
x
e
r
c
i
s
e
3
–
a
l
a
r
g
e
r
s
c
o
p
e
?
•
Every
node
must
point
to
one
and
only
one
node.
•
Then
whether
for
every
node,
it
is
pointed
by
one
and
only
one
node?
•
Every
node
must
point
to
one
and
only
one
node.
•
Every
node
is
pointed
by
no
more
than
one
node.
•
Then
whether
for
every
node,
it
is
pointed
by
one
and
only
one
node?
Sure.
Q
:
solve
this
with
math
induction?
In this set of exercises, various scenarios are discussed related to modeling constraints and assertions within a system. Topics include defining initialization functions, ensuring non-null return values, handling lazy initialization, and exploring different possibilities regarding constraints on nodes. These exercises offer a practical approach to understanding and implementing constraints effectively.
Uploaded on Feb 16, 2025 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Assignment Assignment 4 4 - - Alloy Alloy Shuai Wang shuai.wang@inf.ethz.ch
Exercise 1 Exercise 1 Counter Counter Model Model Define the init function and set n as 0. Increment counter other than last Always greater than or equal to zero. Counter s value never decreases.
Exercise Exercise 2 2 ImageFile ImageFile (eager (eager initialization) initialization) Except File/ImageFile already stored in the state
Exercise Exercise 2 2 ImageFile ImageFile (eager (eager initialization) initialization) Inv1: getImage always returnnon-null. Inv2: getImage always returns the same value. Always return non- null. Always return the same value, for a particular image.
Exercise Exercise 2 2 ImageFile ImageFile (lazy (lazy initialization) initialization) Check if already loaded Two cases to proceed the state from s -> s Lazy initialization
Exercise Exercise 2 2 ImageFile ImageFile (lazy (lazy initialization) initialization) Inv1: getImage always returnnon-null. Inv2: getImage always returns the same value. Shouldn t be null. Always return the same value, for a particular image.
Exercise Exercise 3 3 Assertion Assertion and and Counterexamples Counterexamples Define constraint and assertions for only one node. Every node must point to one and only one node. Then whether for every node, it is pointed by one and only one node? X0,0is a Boolean variable. Given constraint, can we violate the assertion? Solving Boolean constraints are usually super efficient.
Exercise Exercise 3 3 Assertion Assertion and and Counterexamples Counterexamples Definition constraint and assertions for two nodes. All the possibilities. Assertion. Counter example!
Exercise Exercise 3 3 Add Add a a prev edge edge A new fact: Enhancement: Every node is pointed by no more than one node.
Exercise Exercise 3 3 Add Add a a prev edge edge Define constraint and assertions for only one node. Constraint. Assertion. Given constraint, can we violate the assertion?
Exercise Exercise 3 3 Add Add a a prev edge edge Definition constraint and assertions for two nodes. Constraint. Assertion. Given constraint, can we violate the assertion?
Exercise Exercise 3 3 a a larger larger scope? scope? Every node must point to one and only one node. Every node is pointed by no more than one node. Then whether for every node, it is pointed by one and only one node? Sure. Every node must point to one and only one node. Then whether for every node, it is pointed by one and only one node? Q: solve this with math induction?
