Improvements

Author: rcosta358

_sass/custom/custom.scss

@@ -5,9 +5,9 @@
 .site-title {
   display: inline-flex;
   align-items: center;
-  font-weight: 700;
-  font-size: 1.2rem;
-  letter-spacing: 0.01em;
+  font-weight: 500;
+  font-size: 1.4rem;
+  letter-spacing: 0.02em;
   color: #171a1f !important;
 }
 
@@ -51,7 +51,7 @@
   border: 1px solid rgba(38, 48, 68, 0.45);
   border-radius: 1rem;
   background: linear-gradient(180deg, #172033 0%, #111827 100%);
-  box-shadow: 0 18px 36px rgba(15, 23, 42, 0.18);
+  box-shadow: 0 10px 10px rgba(15, 23, 42, 0.15);
 }
 
 .main-content div.highlighter-rouge,
@@ -116,7 +116,7 @@
   fill: currentColor;
 }
 
-.main-content .diagnostic-image {
+.main-content img {
   display: block;
   width: 100%;
   max-width: 100%;
@@ -125,7 +125,7 @@
   border: 1px solid rgba(38, 48, 68, 0.45);
   border-radius: 1rem;
   background: linear-gradient(180deg, #172033 0%, #111827 100%);
-  box-shadow: 0 18px 36px rgba(15, 23, 42, 0.18);
+  box-shadow: 0 10px 10px rgba(15, 23, 42, 0.15);
 }
 
 .main-content pre,

pages/concepts/state-refinements.md

@@ -59,7 +59,7 @@ public class Buffer {
 
 If no `to` transition is declared, LiquidJava defaults the constructor to the first state listed in the corresponding `@StateSet`.
 
-Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won't be able to track the state of the object across method calls, which can lead to unexpected type errors.
+Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won't be able to track the state of the object across method calls.
 
 When refining interfaces, which cannot have a constructor, LiquidJava still needs an initialization point. In those cases, the refinement interface must declare a method whose name matches the class we are refining. For example, an interface named `ArrayListRefinements` that is refining `java.util.ArrayList` should declare the method `public void ArrayList()`. This method plays the role of a constructor for the typestate system and ensures the initial values are set correctly.
 
@@ -88,6 +88,4 @@ public class Device {
 }
 ```
 
-Each state set is exclusive: at any moment, the object can only be in one state from that specific set. In the example above, the object cannot be both `open` and `closed`, and it cannot be both `clean` and `dirty`.
-
-When using more than one state set, the states must be combined with `&&` in the `from` and `to` annotations, as shown in the example above. This is because the object must always be in exactly one state from each set, so we need to specify the full state of the object in the preconditions and postconditions.
+Each state set is **mutually exclusive**: at any given moment, the object must be in exactly one state from each state set. To this end, in state transitions, the states must be combined with `&&` to specify the object's complete state. In the example above, the object cannot be both `open` and `closed`, and it cannot be both `clean` and `dirty`.